structure Lean.Elab.Frontend.State : Type

• commandState : Command.State
• parserState : Parser.ModuleParserState
• cmdPos : String.Pos
• commands : Array Syntax

instance Lean.Elab.Frontend.instNonemptyState : Nonempty State

structure Lean.Elab.Frontend.Context : Type

• inputCtx : Parser.InputContext

@[reducible, inline]

abbrev Lean.Elab.Frontend.FrontendM (α : Type) : Type

def Lean.Elab.Frontend.setCommandState (commandState : Command.State) : FrontendM Unit

@[inline]

def Lean.Elab.Frontend.runCommandElabM {α : Type} (x : Command.CommandElabM α) : FrontendM α

def Lean.Elab.Frontend.elabCommandAtFrontend (stx : Syntax) : FrontendM Unit

def Lean.Elab.Frontend.updateCmdPos : FrontendM Unit

def Lean.Elab.Frontend.getParserState : FrontendM Parser.ModuleParserState

def Lean.Elab.Frontend.getCommandState : FrontendM Command.State

def Lean.Elab.Frontend.setParserState (ps : Parser.ModuleParserState) : FrontendM Unit

def Lean.Elab.Frontend.setMessages (msgs : MessageLog) : FrontendM Unit

def Lean.Elab.Frontend.getInputContext : FrontendM Parser.InputContext

def Lean.Elab.Frontend.processCommand : FrontendM Bool

partial def Lean.Elab.Frontend.processCommands : FrontendM Unit

structure Lean.Elab.IncrementalStateextends Lean.Elab.Frontend.State : Type

• commandState : Command.State
• parserState : Parser.ModuleParserState
• cmdPos : String.Pos
• commands : Array Syntax
• inputCtx : Parser.InputContext
• initialSnap : Language.Lean.CommandParsedSnapshot

instance Lean.Elab.instNonemptyIncrementalState : Nonempty IncrementalState

def Lean.Elab.IO.processCommandsIncrementally (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) (old? : Option IncrementalState) : BaseIO IncrementalState

Variant of IO.processCommands that allows for potential incremental reuse. Pass in the result of a previous invocation done with the same state (but usually different input context) to allow for reuse.

partial def Lean.Elab.IO.processCommandsIncrementally.go (inputCtx : Parser.InputContext) (initialSnap : Language.Lean.CommandParsedSnapshot) (t : Task Language.Lean.CommandParsedSnapshot) (commands : Array Language.Lean.CommandParsedSnapshot) : BaseIO IncrementalState

def Lean.Elab.IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO Frontend.State

def Lean.Elab.process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog)

@[export lean_run_frontend]

def Lean.Elab.runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 0) (oleanFileName? ileanFileName? : Option String := none) (jsonOutput : Bool := false) (errorOnKinds : Array Name := #[]) (plugins : Array System.FilePath := #[]) (printStats : Bool := false) (setupFileName? : Option System.FilePath := none) : IO (Option Environment)