From f13bdd686972013724c70fdd84cc1afbea2b4cfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Apr 2021 14:17:30 -0700 Subject: [PATCH] fix: error recovery at `sepBy` combinator --- src/Lean/Parser/Basic.lean | 2 +- tests/lean/interactive/completion3.lean | 10 ++++++++++ tests/lean/interactive/completion3.lean.expected.out | 8 ++++++++ 3 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 tests/lean/interactive/completion3.lean create mode 100644 tests/lean/interactive/completion3.lean.expected.out diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 7544c3300c..edd32307a3 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -628,7 +628,7 @@ private partial def sepByFnAux (p : ParserFn) (sep : ParserFn) (allowTrailingSep let mut s := p c s if s.hasError then if s.pos > pos then - return s + return s.mkNode nullKind iniSz else if pOpt then let s := s.restore sz pos return s.mkNode nullKind iniSz diff --git a/tests/lean/interactive/completion3.lean b/tests/lean/interactive/completion3.lean new file mode 100644 index 0000000000..6a8c35a779 --- /dev/null +++ b/tests/lean/interactive/completion3.lean @@ -0,0 +1,10 @@ +structure S where + x : Nat + y : String + b : Bool + +def f (s : S) : Nat := + let rec foo (s : S) := + if s. then 1 else 2 + --^ textDocument/completion + foo s diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out new file mode 100644 index 0000000000..36a7274219 --- /dev/null +++ b/tests/lean/interactive/completion3.lean.expected.out @@ -0,0 +1,8 @@ +{"textDocument": {"uri": "file://completion3.lean"}, + "position": {"line": 7, "character": 9}} +{"items": + [{"label": "b", "detail": "S → Bool"}, + {"label": "mk", "detail": "Nat → String → Bool → S"}, + {"label": "x", "detail": "S → Nat"}, + {"label": "y", "detail": "S → String"}], + "isIncomplete": true}