fix: do not create choice nodes for failed parses

leanprover · Nov 4, 2022 · ec8b114 · ec8b114
1 parent 9850e7a
commit ec8b114
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
@@ -1381,8 +1381,7 @@ def keepPrevError (s : ParserState) (oldStackSize : Nat) (oldStopPos : String.Po
 def mergeErrors (s : ParserState) (oldStackSize : Nat) (oldError : Error) : ParserState :=
   match s with
   | ⟨stack, lhsPrec, pos, cache, some err⟩ =>
-    if oldError == err then s
-    else ⟨stack.shrink oldStackSize, lhsPrec, pos, cache, some (oldError.merge err)⟩
+    ⟨stack.shrink oldStackSize, lhsPrec, pos, cache, if oldError == err then some err else some (oldError.merge err)⟩
   | other                         => other
 
 def keepLatest (s : ParserState) (startStackSize : Nat) : ParserState :=

diff --git a/tests/lean/1760.lean b/tests/lean/1760.lean
@@ -0,0 +1,3 @@
+-- should run in linear time
+#check [[[[[[[[[[[[[[[[[[[[[[[[
+#check (((((((((((((((((((((((())))))))))))))))))))))))