diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index e0c1690c1f..a13b52536c 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1469,11 +1469,7 @@ def longestMatchFn (left? : Option Syntax) : List (Parser × Nat) → ParserFn let startLhsPrec := s.lhsPrec let startPos := s.pos let s := runLongestMatchParser left? s.lhsPrec p.1.fn c s - if s.hasError then - let s := s.shrinkStack startSize - longestMatchFnAux left? startSize startLhsPrec startPos p.2 ps c s - else - longestMatchFnAux left? startSize startLhsPrec startPos p.2 ps c s + longestMatchFnAux left? startSize startLhsPrec startPos p.2 ps c s def anyOfFn : List Parser → ParserFn | [], _, s => s.mkError "anyOf: empty list" diff --git a/tests/lean/tokenErrors.lean.expected.out b/tests/lean/tokenErrors.lean.expected.out index c3d95dd62f..5a38dadf3c 100644 --- a/tests/lean/tokenErrors.lean.expected.out +++ b/tests/lean/tokenErrors.lean.expected.out @@ -6,6 +6,7 @@ tokenErrors.lean:14:0: error: unterminated comment tokenErrors.lean:13:0-13:3: error: unexpected doc string failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation) tokenErrors.lean:17:0: error: unterminated comment +tokenErrors.lean:16:0-16:6: error: unknown constant '[anonymous]' inductive Nat : Type constructors: Nat.zero : Nat