From 6dc3e55c54ef27e4e9b397101ff92bb5deedf853 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 4 Apr 2021 23:59:03 +0200 Subject: [PATCH] fix: longestMatchFn: do not discard partial syntax tree of first overload --- src/Lean/Parser/Basic.lean | 6 +----- tests/lean/tokenErrors.lean.expected.out | 1 + 2 files changed, 2 insertions(+), 5 deletions(-) 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