From 69fe4c73388f06e7900d2005b1e85b21efd33261 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 2 Oct 2020 19:11:15 +0200
Subject: [PATCH] fix: formatter: must backtrack on symbols as well

---
 src/Lean/PrettyPrinter/Formatter.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 5adbed5a64..5964e6b29d 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -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