Lean4
/-- `#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
```lean
/-- error: <input>:1:3: Stacks tags must be exactly 4 characters -/
#guard_msgs in #parse Mathlib.Stacks.stacksTagFn => "A05"
```
-/
@[command_parser 1000]
public meta def parseCmd : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.GuardExceptions.parseCmd 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#parse ") (ParserDescr.const✝ `ident))
(ParserDescr.symbol✝ " => "))
(ParserDescr.const✝ `str))
