Documentation

Lean.Elab.Frontend

structure Lean.Elab.Frontend.State :

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

Instances For

Lean.Elab.Frontend.instNonemptyState

instance Lean.Elab.Frontend.instNonemptyState :

Nonempty Lean.Elab.Frontend.State

Equations

Lean.Elab.Frontend.instNonemptyState = ⋯

structure Lean.Elab.Frontend.Context :

inputCtx : Lean.Parser.InputContext

@[reducible, inline]

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

Equations

Lean.Elab.Frontend.FrontendM = ReaderT Lean.Elab.Frontend.Context (StateRefT' IO.RealWorld Lean.Elab.Frontend.State IO)

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

Lean.Elab.Frontend.FrontendM Unit

Equations

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

@[inline]

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

Lean.Elab.Frontend.FrontendM α

Equations

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

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

Lean.Elab.Frontend.FrontendM Unit

Equations

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

def Lean.Elab.Frontend.updateCmdPos :

Lean.Elab.Frontend.FrontendM Unit

Equations

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

def Lean.Elab.Frontend.getParserState :

Lean.Elab.Frontend.FrontendM Lean.Parser.ModuleParserState

Equations

Lean.Elab.Frontend.getParserState = do let __do_lift ← get pure __do_lift.parserState

def Lean.Elab.Frontend.getCommandState :

Lean.Elab.Frontend.FrontendM Lean.Elab.Command.State

Equations

Lean.Elab.Frontend.getCommandState = do let __do_lift ← get pure __do_lift.commandState

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

Lean.Elab.Frontend.FrontendM Unit

Equations

Lean.Elab.Frontend.setParserState ps = modify fun (s : Lean.Elab.Frontend.State) => { commandState := s.commandState, parserState := ps, cmdPos := s.cmdPos, commands := s.commands }

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

Lean.Elab.Frontend.FrontendM Unit

Equations

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

def Lean.Elab.Frontend.getInputContext :

Lean.Elab.Frontend.FrontendM Lean.Parser.InputContext

Equations

Lean.Elab.Frontend.getInputContext = do let __do_lift ← read pure __do_lift.inputCtx

def Lean.Elab.Frontend.processCommand :

Lean.Elab.Frontend.FrontendM Bool

Equations

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

partial def Lean.Elab.Frontend.processCommands :

Lean.Elab.Frontend.FrontendM Unit

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

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

Instances For

Lean.Elab.instNonemptyIncrementalState

instance Lean.Elab.instNonemptyIncrementalState :

Nonempty Lean.Elab.IncrementalState

Equations

Lean.Elab.instNonemptyIncrementalState = ⋯

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

BaseIO Lean.Elab.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.

Equations

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

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

BaseIO Lean.Elab.IncrementalState

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

IO Lean.Elab.Frontend.State

Equations

Lean.Elab.IO.processCommands inputCtx parserState commandState = do let st ← liftM (Lean.Elab.IO.processCommandsIncrementally inputCtx parserState commandState none) pure st.toState

def Lean.Elab.process (input : String) (env : Lean.Environment) (opts : Lean.Options) (fileName : optParam (Option String) none) :

IO (Lean.Environment × Lean.MessageLog)

Equations

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

@[export lean_run_frontend]

def Lean.Elab.runFrontend (input : String) (opts : Lean.Options) (fileName : String) (mainModuleName : Lake.Name) (trustLevel : optParam UInt32 0) (ileanFileName? : optParam (Option String) none) (jsonOutput : optParam Bool false) :

IO (Lean.Environment × Bool)

Equations

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