From 1ac8a4083ffd4b3ae612efee5e6cd06abb5deb71 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 4 Jun 2023 21:09:15 -0400
Subject: [PATCH] feat: report section name in invalid end msg

---
 src/Lean/Elab/BuiltinCommand.lean       | 27 +++++++++++++++----------
 tests/lean/invalidEnd.lean              |  8 ++++++++
 tests/lean/invalidEnd.lean.expected.out |  4 ++++
 3 files changed, 28 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/invalidEnd.lean
 create mode 100644 tests/lean/invalidEnd.lean.expected.out

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 90184b825e..482a45bec8 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -52,14 +52,19 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
   for _ in [0:numScopes] do
     popScope
 
-private def checkAnonymousScope : List Scope → Bool
-  | { header := "", .. } :: _   => true
-  | _                           => false
+private def checkAnonymousScope : List Scope → Option Name
+  | { header := "", .. } :: _ => none
+  | { header := h, .. }  :: _ => some h
+  | _                         => some .anonymous -- should not happen
 
-private def checkEndHeader : Name → List Scope → Bool
-  | .anonymous, _                             => true
-  | .str p s,   { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
-  | _,          _                             => false
+private def checkEndHeader : Name → List Scope → Option Name
+  | .anonymous, _ => none
+  | .str p s, { header := h, .. } :: scopes =>
+    if h == s then
+      (.str · s) <$> checkEndHeader p scopes
+    else
+      some h
+  | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
   match stx with
@@ -94,12 +99,12 @@ private def checkEndHeader : Name → List Scope → Bool
     throwError "invalid 'end', insufficient scopes"
   match header? with
   | none        =>
-    unless checkAnonymousScope scopes do
-      throwError "invalid 'end', name is missing"
+    if let some name := checkAnonymousScope scopes then
+      throwError "invalid 'end', name is missing (expected {name})"
   | some header =>
-    unless checkEndHeader header scopes do
+    if let some name := checkEndHeader header scopes then
       addCompletionInfo <| CompletionInfo.endSection stx (scopes.map fun scope => scope.header)
-      throwError "invalid 'end', name mismatch"
+      throwError "invalid 'end', name mismatch (expected {if name == `«» then `nothing else name})"
 
 private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
   if h : i < cmds.size then
diff --git a/tests/lean/invalidEnd.lean b/tests/lean/invalidEnd.lean
new file mode 100644
index 0000000000..970731d296
--- /dev/null
+++ b/tests/lean/invalidEnd.lean
@@ -0,0 +1,8 @@
+namespace Foo.Bar
+section Baz
+section
+
+end Baz
+end Bal
+end Fool.Bar
+end
diff --git a/tests/lean/invalidEnd.lean.expected.out b/tests/lean/invalidEnd.lean.expected.out
new file mode 100644
index 0000000000..61dfe22e0b
--- /dev/null
+++ b/tests/lean/invalidEnd.lean.expected.out
@@ -0,0 +1,4 @@
+invalidEnd.lean:5:0-5:7: error: invalid 'end', name mismatch (expected nothing)
+invalidEnd.lean:6:0-6:7: error: invalid 'end', name mismatch (expected Baz)
+invalidEnd.lean:7:0-7:12: error: invalid 'end', name mismatch (expected Foo.Bar)
+invalidEnd.lean:8:0-8:3: error: invalid 'end', insufficient scopes