From a076b5b89e3711a986ae3be87331db405796ef37 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Apr 2021 10:24:57 -0700
Subject: [PATCH] feat: improved error recovery for interpolated strings

---
 src/Lean/Parser/Basic.lean                          |  4 ++++
 src/Lean/Parser/StrInterpolation.lean               | 13 ++++++++++---
 tests/lean/interactive/completionIStr.lean          |  7 +++++++
 .../interactive/completionIStr.lean.expected.out    |  7 +++++++
 4 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/interactive/completionIStr.lean
 create mode 100644 tests/lean/interactive/completionIStr.lean.expected.out

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index b7367412f9..26cfbe6570 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -244,6 +244,10 @@ def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : P
     let stack   := stack.push newNode
     ⟨stack, lhsPrec, pos, cache, err⟩
 
+def setError (s : ParserState) (msg : String) : ParserState :=
+  match s with
+  | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
+
 def mkError (s : ParserState) (msg : String) : ParserState :=
   match s with
   | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
diff --git a/src/Lean/Parser/StrInterpolation.lean b/src/Lean/Parser/StrInterpolation.lean
index 7ea6a3e907..b2bc9453f4 100644
--- a/src/Lean/Parser/StrInterpolation.lean
+++ b/src/Lean/Parser/StrInterpolation.lean
@@ -15,7 +15,8 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
   let rec parse (startPos : Nat) (c : ParserContext) (s : ParserState) : ParserState :=
     let i     := s.pos
     if input.atEnd i then
-      s.mkUnexpectedErrorAt "unterminated string literal" startPos
+      let s := s.mkNode interpolatedStrKind stackSize
+      s.setError "unterminated string literal"
     else
       let curr := input.get i
       let s    := s.setPos (input.next i)
@@ -29,8 +30,14 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
         let s := p c s
         if s.hasError then s
         else
-          let pos := s.pos
-          andthenFn (satisfyFn (· == '}') "expected '}'") (parse pos) c s
+          let i := s.pos
+          let curr := input.get i
+          if curr == '}' then
+            let s := s.setPos (input.next i)
+            parse i c s
+          else
+            let s := s.mkNode interpolatedStrKind stackSize
+            s.setError "expected '}'"
       else
         parse startPos c s
   let startPos := s.pos
diff --git a/tests/lean/interactive/completionIStr.lean b/tests/lean/interactive/completionIStr.lean
new file mode 100644
index 0000000000..49c205940c
--- /dev/null
+++ b/tests/lean/interactive/completionIStr.lean
@@ -0,0 +1,7 @@
+structure C where
+  f1 : Nat
+  f2 : Bool
+  b1 : String
+
+#check fun c : C => s!"testing {c. "
+                                --^ textDocument/completion
diff --git a/tests/lean/interactive/completionIStr.lean.expected.out b/tests/lean/interactive/completionIStr.lean.expected.out
new file mode 100644
index 0000000000..8a6c3b8354
--- /dev/null
+++ b/tests/lean/interactive/completionIStr.lean.expected.out
@@ -0,0 +1,7 @@
+{"textDocument": {"uri": "file://completionIStr.lean"},
+ "position": {"line": 5, "character": 34}}
+{"items":
+ [{"label": "b1", "detail": "C → String"},
+  {"label": "f1", "detail": "C → Nat"},
+  {"label": "f2", "detail": "C → Bool"}],
+ "isIncomplete": true}