#parse -- a command to parse text and log outputs

def Mathlib.GuardExceptions.captureException (env : Lean.Environment) (s : Lean.Parser.ParserFn) (input : String) : Except String Lean.Syntax

captureException env s input uses the given Environment env to parse the String input using the ParserFn s.

This is a variation of Lean.Parser.runParserCategory.

Equations

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

def Mathlib.GuardExceptions.parseAsTacticSeq (env : Lean.Environment) (input : String) (fileName : String := "<input>") : Except String (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Parse a string as a tactic sequence.

This is a slight modification of Parser.runParserCategory.

Equations

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

def Mathlib.GuardExceptions.parseCmd : Lean.ParserDescr

#parse parserFnId => str allows to capture parsing exceptions. parserFnId is the identifier of a ParserFn and str is the string that parserFnId should parse.

If the parse is successful, then the output is logged; if the parse is successful, then the output is captured in an exception.

In either case, #guard_msgs can then be used to capture the resulting parsing errors.

For instance, #parse can be used as follows

/-- error: <input>:1:3: Stacks tags must be exactly 4 characters -/
#guard_msgs in #parse Mathlib.Stacks.stacksTagFn => "A05"

Equations

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