From b581c2fa17062fce3b5b18b8f4685f97893ac9cb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 Jul 2022 19:12:53 -0400
Subject: [PATCH] fix: `evalTactic`

Another bug reported by Patrick.
---
 src/Lean/Elab/Tactic/Basic.lean                     | 12 ++++++------
 tests/lean/interactive/hover.lean                   |  2 +-
 tests/lean/interactive/infoIssues.lean.expected.out | 12 ++----------
 tests/lean/interactive/plainGoal.lean.expected.out  |  3 +--
 4 files changed, 10 insertions(+), 19 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 299778746e..7021483c5d 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -100,8 +100,8 @@ def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
 protected def saveState : TacticM SavedState :=
   return { term := (← Term.saveState), tactic := (← get) }
 
-def SavedState.restore (b : SavedState) : TacticM Unit := do
-  b.term.restore
+def SavedState.restore (b : SavedState) (restoreInfo := false) : TacticM Unit := do
+  b.term.restore restoreInfo
   set b.tactic
 
 protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Core.Context).currMacroScope
@@ -170,7 +170,7 @@ where
      let exs := failures.filterMap fun | .abort _ => none | .exception ex => some ex
      if exs.isEmpty then
        if let some (.abort s) := failures.find? fun | .abort _ => true | _ => false then
-         s.restore
+         s.restore (restoreInfo := true)
          throwAbortTactic
        else
          throwErrorAt stx "unexpected syntax {indentD stx}" 
@@ -181,14 +181,14 @@ where
 
     @[inline] handleEx (s : SavedState) (failures : Array EvalTacticFailure) (ex : Exception) (k : Array EvalTacticFailure → TacticM Unit) := do
       match ex with
-      | .error .. => s.restore; k (failures.push (.exception ex))
+      | .error .. => s.restore (restoreInfo := true); k (failures.push (.exception ex))
       | .internal id _ =>
         if id == unsupportedSyntaxExceptionId then
           -- We do not store `unsupportedSyntaxExceptionId`, see throwExs
-          s.restore; k failures
+          s.restore (restoreInfo := true); k failures
         else if id == abortTacticExceptionId then
           let failures := failures.push (.abort (← Tactic.saveState))
-          s.restore; k failures
+          s.restore (restoreInfo := true); k failures
         else
           throw ex -- (*)
 
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 6e7f2b0c7d..876fcb994b 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -26,7 +26,7 @@ example : True := by
 
 /-- My way better tactic -/
 macro_rules
-  | `(tactic| mytac $[only]? $e) => `(apply $e)
+  | `(tactic| mytac $[only]? $e) => `(tactic| apply $e)
 
 example : True := by
   mytac only True.intro
diff --git a/tests/lean/interactive/infoIssues.lean.expected.out b/tests/lean/interactive/infoIssues.lean.expected.out
index d7012c79dc..c8085552c1 100644
--- a/tests/lean/interactive/infoIssues.lean.expected.out
+++ b/tests/lean/interactive/infoIssues.lean.expected.out
@@ -13,22 +13,14 @@
   "p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
 {"textDocument": {"uri": "file://infoIssues.lean"},
  "position": {"line": 13, "character": 36}}
-{"rendered":
- "```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + (0 + Nat.succ n✝)\n```\n---\n```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + Nat.succ n✝\n```",
- "goals":
- ["p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + (0 + Nat.succ n✝)",
-  "p : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 0 + Nat.succ n✝"]}
+{"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file://infoIssues.lean"},
  "position": {"line": 15, "character": 2}}
 {"rendered": "```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```",
  "goals": ["case right\np : Prop\nx : Nat\n⊢ p"]}
 {"textDocument": {"uri": "file://infoIssues.lean"},
  "position": {"line": 25, "character": 35}}
-{"rendered":
- "```lean\np : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (y + 1))\n```\n---\n```lean\np : Prop\nx y : Nat\n⊢ y + 1 = 0 + (y + 1)\n```",
- "goals":
- ["p : Prop\nx y : Nat\n⊢ y + 1 = 0 + (0 + (y + 1))",
-  "p : Prop\nx y : Nat\n⊢ y + 1 = 0 + (y + 1)"]}
+{"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file://infoIssues.lean"},
  "position": {"line": 25, "character": 9}}
 {"rendered":
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 2e5f21d06e..6ebe5e48c1 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -90,10 +90,9 @@
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 76, "character": 29}}
 {"rendered":
- "```lean\nt a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * Nat.succ n✝\n```\n---\n```lean\nt a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```\n---\n```lean\nt a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```",
+ "```lean\nt a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * Nat.succ n✝\n```\n---\n```lean\nt a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```",
  "goals":
  ["t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * Nat.succ n✝",
-  "t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)",
   "t a n✝ : Nat\n: t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 80, "character": 53}}