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.

opaque Lean.Server.Snapshots.dummyTacticCache : IO.Ref Lean.Elab.Tactic.Cache

structure Lean.Server.Snapshots.Snapshot : Type

• 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
• interactiveDiags : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic

  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 $/lean/interactiveDiagnostics.

• tacticCache : IO.Ref Lean.Elab.Tactic.Cache

What Lean knows about the world after the header and each command.

def Lean.Server.Snapshots.Snapshot.endPos (s : Lean.Server.Snapshots.Snapshot) : String.Pos

def Lean.Server.Snapshots.Snapshot.env (s : Lean.Server.Snapshots.Snapshot) : Lean.Environment

def Lean.Server.Snapshots.Snapshot.msgLog (s : Lean.Server.Snapshots.Snapshot) : Lean.MessageLog

def Lean.Server.Snapshots.Snapshot.diagnostics (s : Lean.Server.Snapshots.Snapshot) : Lean.PersistentArray Lean.Lsp.Diagnostic

def Lean.Server.Snapshots.Snapshot.infoTree (s : Lean.Server.Snapshots.Snapshot) : Lean.Elab.InfoTree

def Lean.Server.Snapshots.Snapshot.isAtEnd (s : Lean.Server.Snapshots.Snapshot) : Bool

def Lean.Server.Snapshots.Snapshot.runCommandElabM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (meta : Lean.Server.DocumentMeta) (c : Lean.Elab.Command.CommandElabM α) : EIO Lean.Exception α

Use the command state in the given snapshot to run a CommandElabM.

def Lean.Server.Snapshots.Snapshot.runCoreM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (meta : Lean.Server.DocumentMeta) (c : Lean.CoreM α) : EIO Lean.Exception α

Run a CoreM computation using the data in the given snapshot.

def Lean.Server.Snapshots.Snapshot.runTermElabM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (meta : Lean.Server.DocumentMeta) (c : Lean.Elab.TermElabM α) : EIO Lean.Exception α

Run a TermElabM computation using the data in the given snapshot.

def Lean.Server.Snapshots.parseNextCmd (inputCtx : Lean.Parser.InputContext) (snap : Lean.Server.Snapshots.Snapshot) : IO Lean.Syntax

Parses the next command occurring after the given snapshot without elaborating it.

opaque Lean.Server.Snapshots.server.stderrAsMessages : Lean.Option Bool

def Lean.Server.Snapshots.compileNextCmd (inputCtx : Lean.Parser.InputContext) (snap : Lean.Server.Snapshots.Snapshot) (hasWidgets : Bool) : IO Lean.Server.Snapshots.Snapshot

Compiles the next command occurring after the given snapshot. If there is no next command (file ended), Snapshot.isAtEnd will hold of the return value.

def Lean.Server.Snapshots.compileNextCmd.withNewInteractiveDiags (inputCtx : Lean.Parser.InputContext) (snap : Lean.Server.Snapshots.Snapshot) (hasWidgets : Bool) (msgLog : Lean.MessageLog) : IO (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic)

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.