feat: better error recovery for match syntax

src/Lean/Elab/Quotation.lean

@@ -406,7 +406,9 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
   trace[Elab.match_syntax] "match {discrs} with {alts}"
   match discrs, alts with
   | [],            ([], rhs)::_ => pure rhs  -- nothing left to match
-  | _,             []           => throwError "non-exhaustive 'match' (syntax)"
+  | _,             []           =>
+   logError "non-exhaustive 'match' (syntax)"
+   pure Syntax.missing
   | discr::discrs, alt::alts    => do
     let info ← getHeadInfo alt
     let pat  := alt.1.head!

tests/lean/interactive/matchStxCompletion.lean

@@ -0,0 +1,10 @@
+structure C where
+  f1 : Nat
+  f2 : Bool
+  b1 : String
+
+def f (x : Lean.Syntax) (y : C) : IO Nat := do
+  match x with
+  | `($a + 1) =>
+    if y.
+       --^ textDocument/completion

tests/lean/interactive/matchStxCompletion.lean.expected.out

@@ -0,0 +1,7 @@
+{"textDocument": {"uri": "file://matchStxCompletion.lean"},
+ "position": {"line": 8, "character": 9}}
+{"items":
+ [{"label": "b1", "detail": "C → String"},
+  {"label": "f1", "detail": "C → Nat"},
+  {"label": "f2", "detail": "C → Bool"}],
+ "isIncomplete": true}