diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 53cc606830..3b73da2e8f 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index df93d42b28..ade2b8e3bf 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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