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.

structure Lean.Server.Snapshots.Snapshot : Type

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

• stx : Syntax
• mpState : Parser.ModuleParserState
• cmdState : Elab.Command.State

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

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

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

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

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

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

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

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

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

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

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