One can think of this module as being a partial reimplementation of Lean.Elab.Frontend which also stores a snapshot of the world after each command. Importantly, we allow (re)starting compilation from any snapshot/position in the file for interactive editing purposes.
- beginPos : String.Pos
Where the command which produced this snapshot begins. Note that neighbouring snapshots are not necessarily attached beginning-to-end, since inputs outside the grammar advance the parser but do not produce snapshots.
- stx : Lean.Syntax
- mpState : Lean.Parser.ModuleParserState
- cmdState : Lean.Elab.Command.State
We cache interactive diagnostics in order not to invoke the pretty-printer again on messages from previous snapshots when publishing diagnostics for every new snapshot (this is quadratic), as well as not to invoke it once again when handling
What Lean knows about the world after the header and each command.
Compiles the next command occurring after the given snapshot. If there is no next command
Snapshot.isAtEnd will hold of the return value.
Compute the current interactive diagnostics log by finding a "diff" relative to the parent
snapshot. We need to do this because unlike the
MessageLog itself, interactive diags are not
part of the command state.