From 78a2de4241b0dffc588d8bd870e653aef582a74f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 May 2021 16:07:27 -0700
Subject: [PATCH] feat: better error recovery for `match` syntax

---
 src/Lean/Elab/Quotation.lean                           |  4 +++-
 tests/lean/interactive/matchStxCompletion.lean         | 10 ++++++++++
 .../interactive/matchStxCompletion.lean.expected.out   |  7 +++++++
 3 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/interactive/matchStxCompletion.lean
 create mode 100644 tests/lean/interactive/matchStxCompletion.lean.expected.out

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 191aea46bc..4076041fc9 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/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!
diff --git a/tests/lean/interactive/matchStxCompletion.lean b/tests/lean/interactive/matchStxCompletion.lean
new file mode 100644
index 0000000000..24f92d7a69
--- /dev/null
+++ b/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
diff --git a/tests/lean/interactive/matchStxCompletion.lean.expected.out b/tests/lean/interactive/matchStxCompletion.lean.expected.out
new file mode 100644
index 0000000000..76851c27da
--- /dev/null
+++ b/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}