max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: pretty printer: tolerate missing better

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-05 14:46:05 +02:00
parent 76c66fc4d4
commit 456264bf31
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -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 "<missing>"
goLeft
else
let f ← runForNodeKind formatterAttribute k interpretParserDescr'
f
@[implementedBy formatterForKindUnsafe]
constant formatterForKind (k : SyntaxNodeKind) : Formatter

6
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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