max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: syntax not updating in header snapshots

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-08-12 20:11:43 -04:00 • committed by Leonardo de Moura
parent ce7f31a654
commit c316a8ea69
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Server/Snapshots.lean
View file

@ -32,7 +32,8 @@ structure Snapshot where
namespace Snapshot
def endPos (s : Snapshot) : String.Pos := s.mpState.pos
def endPos (s : Snapshot) : String.Pos :=
s.mpState.pos
def env (s : Snapshot) : Environment :=
s.cmdState.env
@ -42,10 +43,11 @@ def msgLog (s : Snapshot) : MessageLog :=
end Snapshot
/-- Reparses the header syntax but does not re-elaborate it. Used to ignore whitespace-only changes. -/
def reparseHeader (contents : String) (header : Snapshot) (opts : Options := {}) : IO Snapshot := do
let inputCtx := Parser.mkInputContext contents "<input>"
let (_, newHeaderParserState, _) ← Parser.parseHeader inputCtx
pure { header with mpState := newHeaderParserState }
let (newStx, newMpState, _) ← Parser.parseHeader inputCtx
pure { header with stx := newStx, mpState := newMpState }
private def ioErrorFromEmpty (ex : Empty) : IO.Error :=
nomatch ex