diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 63d7f66db3..56508c7337 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -159,7 +159,12 @@ constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (a constant interpretParserDescr' : ParserDescr → CoreM Formatter unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do - (← liftM $ runForNodeKind formatterAttribute k interpretParserDescr') + if k == `missing then + push "" + goLeft + else + let f ← runForNodeKind formatterAttribute k interpretParserDescr' + f @[implementedBy formatterForKindUnsafe] constant formatterForKind (k : SyntaxNodeKind) : Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index a47898ef0e..fb7615a4b6 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -269,7 +269,11 @@ constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do - (← liftM $ runForNodeKind parenthesizerAttribute k interpretParserDescr') + if k == `missing then + pure () + else + let p ← runForNodeKind parenthesizerAttribute k interpretParserDescr' + p @[implementedBy parenthesizerForKindUnsafe] constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer