fix: evalTactic

Another bug reported by Patrick.

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 -- (*)
 

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

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":

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