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

fix: formatter: must backtrack on symbols as well

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-02 19:11:15 +02:00
parent 21f1a66ceb
commit 69fe4c7338
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -264,8 +264,13 @@ else do {
@[combinatorFormatter symbol]
def symbol.formatter (sym : String) : Formatter := do
pushToken sym;
goLeft
stx ← getCur;
if stx.isToken sym then do
pushToken sym;
goLeft
else do
trace! `PrettyPrinter.format.backtrack ("unexpected syntax '" ++ stx ++ "', expected symbol '" ++ sym ++ "'");
throwBacktrack
@[combinatorFormatter symbolNoWs] def symbolNoWs.formatter := symbol.formatter
@[combinatorFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter