chore: add support for error parser in the pretty printer

This commit is contained in:
Leonardo de Moura 2020-10-15 16:31:35 -07:00
parent f36f7592e6
commit e2ecefb67b
2 changed files with 8 additions and 0 deletions

View file

@ -191,6 +191,10 @@ st ← get;
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset);
categoryParser.formatter stx.getId
@[combinatorFormatter Lean.Parser.error]
def error.formatter (msg : String) : Formatter :=
pure ()
@[combinatorFormatter Lean.Parser.try]
def try.formatter (p : Formatter) : Formatter :=
p

View file

@ -320,6 +320,10 @@ def level.parenthesizer : CategoryParenthesizer | prec => do
maybeParenthesize `level (fun stx => Unhygienic.run `(level|($stx))) prec $
parenthesizeCategoryCore `level prec
@[combinatorParenthesizer Lean.Parser.error]
def error.parenthesizer (msg : String) : Parenthesizer :=
pure ()
@[combinatorParenthesizer Lean.Parser.try]
def try.parenthesizer (p : Parenthesizer) : Parenthesizer :=
p