fix: save all info nodes during backtracking

src/Lean/Elab/Term.lean

@@ -194,19 +194,11 @@ protected def saveState : TermElabM SavedState := do
 
 def SavedState.restore (s : SavedState) : TermElabM Unit := do
   let traceState ← getTraceState -- We never backtrack trace message
-  -- We also preserve `TacticInfo` nodes to be able to display the tactic state of broken tactic scripts
-  let infoStateNew := (← get).infoState
-  let oldInfoSize  := s.elab.infoState.trees.size
+  let infoState := (← get).infoState -- We also do not backtrack the info nodes
   s.meta.restore
   set s.elab
   setTraceState traceState
-  -- Add new `TacticInfo` nodes back to restored `infoState`
-  modify fun s => { s with
-    infoState.trees := infoStateNew.trees.foldl (init := s.infoState.trees) (start := oldInfoSize) fun trees info =>
-      match info with
-      | InfoTree.node (Info.ofTacticInfo _) _ => trees.push info
-      | _ => trees
-  }
+  modify fun s => { s with infoState := infoState }
 
 instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState

tests/lean/interactive/haveInfo.lean

@@ -0,0 +1,6 @@
+example : False := by
+  have True by
+    skip
+  --^ $/lean/plainGoal
+    skip
+  admit

tests/lean/interactive/haveInfo.lean.expected.out

@@ -0,0 +1,3 @@
+{"textDocument": {"uri": "file://haveInfo.lean"},
+ "position": {"line": 2, "character": 4}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}