def Lean.Parser.Module.updateTokens (tokens : TokenTable) : TokenTable

structure Lean.Parser.ModuleParserState : Type

• pos : String.Pos.Raw
• recovering : Bool
• hasLeading : Bool

  Whether there is leading whitespace before pos. Used to associate whitespace at the start of the file with the first token of the file.

@[instance_reducible]

instance Lean.Parser.instInhabitedModuleParserState : Inhabited ModuleParserState

def Lean.Parser.parseHeader (inputCtx : InputContext) : IO (TSyntax `Lean.Parser.Module.header × ModuleParserState × MessageLog)

def Lean.Parser.isTerminalCommand (s : Syntax) : Bool

def Lean.Parser.topLevelCommandParserFn : ParserFn

def Lean.Parser.parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog

def Lean.Parser.testParseModuleAux (env : Environment) (inputCtx : InputContext) (s : ModuleParserState) (msgs : MessageLog) (stxs : Array Syntax) : IO (Array Syntax)

def Lean.Parser.testParseModule (env : Environment) (fname contents : String) : IO Syntax

def Lean.Parser.testParseFile (env : Environment) (fname : System.FilePath) : IO Syntax