Lean.Server.Snapshots

source

structure Lean.Server.Snapshots.Snapshot :

Type

beginPos : String.Pos
stx : Lean.Syntax
mpState : Lean.Parser.ModuleParserState
cmdState : Lean.Elab.Command.State
interactiveDiags : Std.PersistentArray Lean.Widget.InteractiveDiagnostic

source

instance Lean.Server.Snapshots.instInhabitedSnapshot :

Inhabited Lean.Server.Snapshots.Snapshot

Equations

Lean.Server.Snapshots.instInhabitedSnapshot = { default := { beginPos := default, stx := default, mpState := default, cmdState := default, interactiveDiags := default } }

source

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

String.Pos

Equations

Lean.Server.Snapshots.Snapshot.endPos s = s.mpState.pos

source

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

Lean.Environment

Equations

Lean.Server.Snapshots.Snapshot.env s = s.cmdState.env

source

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

Lean.MessageLog

Equations

Lean.Server.Snapshots.Snapshot.msgLog s = s.cmdState.messages

source

def Lean.Server.Snapshots.Snapshot.diagnostics (s : Lean.Server.Snapshots.Snapshot) :

Std.PersistentArray Lean.Lsp.Diagnostic

Equations

Lean.Server.Snapshots.Snapshot.diagnostics s = Std.PersistentArray.map (fun d => Lean.Widget.InteractiveDiagnostic.toDiagnostic d) s.interactiveDiags

source

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

Lean.Elab.InfoTree

Equations

Lean.Server.Snapshots.Snapshot.infoTree s = if (s.cmdState.infoState.trees.size == 1) = true then Std.PersistentArray.getOp s.cmdState.infoState.trees 0 else panicWithPosWithDecl "Lean.Server.Snapshots" "Lean.Server.Snapshots.Snapshot.infoTree" 55 2 ("assertion violation: " ++ "s.cmdState.infoState.trees.size == 1\n ")

source

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

Bool

Equations

Lean.Server.Snapshots.Snapshot.isAtEnd s = (Lean.Parser.isEOI s.stx || Lean.Parser.isExitCommand s.stx)

source

def Lean.Server.Snapshots.reparseHeader (contents : String) (header : Lean.Server.Snapshots.Snapshot) (opts : optParam Lean.Options { entries := [] }) :

IO Lean.Server.Snapshots.Snapshot

Equations

Lean.Server.Snapshots.reparseHeader contents header opts = let inputCtx := Lean.Parser.mkInputContext contents ""; do let discr ← Lean.Parser.parseHeader inputCtx let x : Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog := discr match x with | (newStx, newMpState, x) => pure { beginPos := header.beginPos, stx := newStx, mpState := newMpState, cmdState := header.cmdState, interactiveDiags := header.interactiveDiags }

source

def Lean.Server.Snapshots.parseNextCmd (contents : String) (snap : Lean.Server.Snapshots.Snapshot) :

IO Lean.Syntax

Equations

Lean.Server.Snapshots.parseNextCmd contents snap = let inputCtx := Lean.Parser.mkInputContext contents ""; let cmdState := snap.cmdState; let scope := List.head! cmdState.scopes; let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }; let x := Lean.Parser.parseCommand inputCtx pmctx snap.mpState (Lean.Server.Snapshots.Snapshot.msgLog snap); match x with | (cmdStx, x, x_1) => pure cmdStx

source

def Lean.Server.Snapshots.parseAhead (contents : String) (snap : Lean.Server.Snapshots.Snapshot) :

IO (Array Lean.Syntax)

Equations

Lean.Server.Snapshots.parseAhead contents snap = (fun go => let inputCtx := Lean.Parser.mkInputContext contents ""; let cmdState := snap.cmdState; let scope := List.head! cmdState.scopes; let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }; go inputCtx pmctx snap.mpState #[]) (Lean.Server.Snapshots.parseAhead.go snap)

source

partial def Lean.Server.Snapshots.parseAhead.go (snap : Lean.Server.Snapshots.Snapshot) (inputCtx : Lean.Parser.InputContext) (pmctx : Lean.Parser.ParserModuleContext) (cmdParserState : Lean.Parser.ModuleParserState) (stxs : Array Lean.Syntax) :

IO (Array Lean.Syntax)

source

def Lean.Server.Snapshots.compileNextCmd (text : Lean.FileMap) (snap : Lean.Server.Snapshots.Snapshot) (hasWidgets : Bool) :

IO Lean.Server.Snapshots.Snapshot

Equations

Lean.Server.Snapshots.compileNextCmd text snap hasWidgets = (fun withNewInteractiveDiags => let inputCtx := Lean.Parser.mkInputContext text.source ""; let cmdState := snap.cmdState; let scope := List.head! cmdState.scopes; let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }; let x := Lean.Parser.parseCommand inputCtx pmctx snap.mpState (Lean.Server.Snapshots.Snapshot.msgLog snap); match x with | (cmdStx, cmdParserState, msgLog) => let cmdPos := Option.get! (Lean.Syntax.getPos? cmdStx); if (Lean.Parser.isEOI cmdStx || Lean.Parser.isExitCommand cmdStx) = true then do let a ← withNewInteractiveDiags msgLog let endSnap : Lean.Server.Snapshots.Snapshot := { beginPos := cmdPos, stx := cmdStx, mpState := cmdParserState, cmdState := snap.cmdState, interactiveDiags := a } pure endSnap else do let cmdStateRef ← liftM (IO.mkRef (let src := snap.cmdState; { env := src.env, messages := msgLog, scopes := src.scopes, nextMacroScope := src.nextMacroScope, maxRecDepth := src.maxRecDepth, nextInstIdx := src.nextInstIdx, ngen := src.ngen, infoState := src.infoState, traceState := src.traceState })) let cmdCtx : Lean.Elab.Command.Context := { fileName := inputCtx.fileName, fileMap := inputCtx.fileMap, currRecDepth := 0, cmdPos := Lean.Server.Snapshots.Snapshot.endPos snap, macroStack := [], currMacroScope := Lean.firstFrontendMacroScope, ref := Lean.Syntax.missing } let discr ← IO.FS.withIsolatedStreams (liftM (Lean.Elab.Command.catchExceptions (SeqRight.seqRight Lean.Elab.getResetInfoTrees fun x => Lean.Elab.Command.elabCommandTopLevel cmdStx) cmdCtx cmdStateRef)) let x : String × Unit := discr match x with | (output, x) => do let postCmdState ← ST.Ref.get cmdStateRef let _do_jp : Lean.Elab.Command.State → PUnit → IO Lean.Server.Snapshots.Snapshot := fun postCmdState y => do let a ← withNewInteractiveDiags postCmdState.messages let postCmdSnap : Lean.Server.Snapshots.Snapshot := { beginPos := cmdPos, stx := cmdStx, mpState := cmdParserState, cmdState := postCmdState, interactiveDiags := a } pure postCmdSnap if (!String.isEmpty output) = true then let postCmdState := { env := postCmdState.env, messages := Lean.MessageLog.add { fileName := inputCtx.fileName, pos := Lean.FileMap.toPosition inputCtx.fileMap (Lean.Server.Snapshots.Snapshot.endPos snap), endPos := none, severity := Lean.MessageSeverity.information, caption := "", data := Function.comp Lean.MessageData.ofFormat Lean.format output } postCmdState.messages, scopes := postCmdState.scopes, nextMacroScope := postCmdState.nextMacroScope, maxRecDepth := postCmdState.maxRecDepth, nextInstIdx := postCmdState.nextInstIdx, ngen := postCmdState.ngen, infoState := postCmdState.infoState, traceState := postCmdState.traceState }; do let y ← pure PUnit.unit _do_jp postCmdState y else do let y ← pure PUnit.unit _do_jp postCmdState y) (Lean.Server.Snapshots.compileNextCmd.withNewInteractiveDiags text snap hasWidgets)

source

def Lean.Server.Snapshots.compileNextCmd.withNewInteractiveDiags (text : Lean.FileMap) (snap : Lean.Server.Snapshots.Snapshot) (hasWidgets : Bool) (msgLog : Lean.MessageLog) :

IO (Std.PersistentArray Lean.Widget.InteractiveDiagnostic)

Equations

Lean.Server.Snapshots.compileNextCmd.withNewInteractiveDiags text snap hasWidgets msgLog = let newMsgCount := msgLog.msgs.size - (Lean.Server.Snapshots.Snapshot.msgLog snap).msgs.size; let ret := snap.interactiveDiags; do let r ← let col := List.iota newMsgCount; forIn col ret fun i r => let ret := r; let newMsg := Std.PersistentArray.get! msgLog.msgs (msgLog.msgs.size - i); do let a ← Lean.Widget.msgToInteractiveDiagnostic text newMsg hasWidgets let ret : Std.PersistentArray Lean.Widget.InteractiveDiagnostic := Std.PersistentArray.push ret a pure PUnit.unit pure (ForInStep.yield ret) let x : Std.PersistentArray Lean.Widget.InteractiveDiagnostic := r let ret : Std.PersistentArray Lean.Widget.InteractiveDiagnostic := x pure ret