feat: improved error recovery for interpolated strings

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 ] }⟩

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

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

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}