Documentation

Lean.Elab.Frontend

structure Lean.Elab.Frontend.State:

Type

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

structure Lean.Elab.Frontend.Context:

Type

inputCtx : Lean.Parser.InputContext

@[inline]

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

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

Lean.Elab.Frontend.setCommandState commandState = modify fun s => { commandState := commandState, parserState := s.parserState, cmdPos := s.cmdPos, commands := s.commands }

@[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

Lean.Elab.Frontend.elabCommandAtFrontend stx = Lean.Elab.Frontend.runCommandElabM (Lean.Elab.Command.elabCommandTopLevel stx)

def Lean.Elab.Frontend.updateCmdPos:

Lean.Elab.Frontend.FrontendM Unit

Equations

Lean.Elab.Frontend.updateCmdPos = modify fun s => { commandState := s.commandState, parserState := s.parserState, cmdPos := s.parserState.pos, commands := s.commands }

def Lean.Elab.Frontend.getParserState:

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

Equations

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

def Lean.Elab.Frontend.getCommandState:

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

Equations

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

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

Lean.Elab.Frontend.FrontendM Unit

Equations

Lean.Elab.Frontend.setParserState ps = modify fun s => { 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 a ← read pure a.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

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

IO Lean.Elab.Frontend.State

Equations

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

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.

def Lean.Elab.getPrintMessageEndPos (opts : Lean.Options) :

Equations

Lean.Elab.getPrintMessageEndPos opts = Lean.KVMap.getBool opts `printMessageEndPos

@[export lean_run_frontend]

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

IO (Lean.Environment × Bool)

Equations

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