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

Equations

• s.endPos = s.mpState.pos

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

Equations

• s.env = s.cmdState.env

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

Equations

• s.msgLog = s.cmdState.messages

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• s.isAtEnd = Lean.Parser.isTerminalCommand s.stx

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• snap.runCoreM meta c = snap.runCommandElabM meta (Lean.Elab.Command.liftCoreM c)

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.

Equations

• snap.runTermElabM meta c = snap.runCommandElabM meta (Lean.Elab.Command.liftTermElabM c)