From 456264bf316717e039ce9473dd86fd4c5d2cfc11 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 5 May 2021 14:46:05 +0200 Subject: [PATCH] chore: pretty printer: tolerate `missing` better --- src/Lean/PrettyPrinter/Formatter.lean | 7 ++++++- src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +++++- 2 files changed, 11 insertions(+), 2 deletions(-) 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