fix: do not show states from tactics indented further than the cursor

src/Lean/Server/InfoUtils.lean

@@ -226,6 +226,9 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
   t.deepestNodes fun
     | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
+        -- Ignore tactics that are more indented than the cursor position.
+        -- This ensures we get the right state after e.g. deindenting after completing a `have` proof.
+        guard <| (text.toPosition pos).column <= (text.toPosition hoverPos).column
         let trailSize := i.stx.getTrailingSize
         -- show info at EOF even if strictly outside token + trail
         let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx

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

@@ -9,4 +9,5 @@
 {"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
 {"textDocument": {"uri": "file://haveInfo.lean"},
  "position": {"line": 23, "character": 2}}
-{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"rendered": "```lean\nthis : True\n⊢ False\n```",
+ "goals": ["this : True\n⊢ False"]}

tests/lean/interactive/infoIssues.lean

@@ -1,28 +1,30 @@
-#exit
-
+set_option trace.Elab.info true
 example (x y : Nat) (h : x = y) : 0 + x = y + 0 := by
   have := by exact h.symm
-  /-
-    Bad: we get "Goals accomplished" here
-    Should be:
-    ... |- 0 + x = y + 0
-  -/
+--
+--^ $/lean/plainGoal
+-- Good: ..., this : y = x |- 0 + x = y + 0
 
 example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
   constructor
   · cases x
-    next => rfl                --v Good: we get multiple states here as expected
-    next => repeat rw [Nat.zero_add] /- Good: we get the correct behavior here: Goals accomplished. -/
-  /-
-    Bad: We get "Goals accomplished" here
-    Should be:
-    ... |- p
-  -/
+    next => rfl
+                               -- Good: we get multiple states here as expected
+                               --v $/lean/plainGoal
+    next => repeat rw [Nat.zero_add]
+                                  --^ $/lean/plainGoal
+                                  -- Bad? We still get all states except the one closed by implicit `rfl`
+--^ $/lean/plainGoal
+-- Good: ... |- p
 
 example (x : Nat) : x = 0 + (0 + (0 + x)) ∧ p := by
   constructor
   match x with
   | 0 => rfl
-  | y+1 => repeat rw [Nat.zero_add] /- Good: We get the correct behavior here: Goals accomplished. -/
-       --^ Bad: get the `match` tactic initial state here.
-  -- Bad: we get "Goals accomplished" here
+                                 -- Bad? We still get all states except the one closed by implicit `rfl`
+                                 --v $/lean/plainGoal
+  | y+1 => repeat rw [Nat.zero_add]
+       --^ $/lean/plainGoal
+       -- Bad: get the `match` tactic initial state here.
+--^ $/lean/plainGoal
+-- Good:  ... |- p

tests/lean/interactive/infoIssues.lean.expected.out

@@ -1,2 +1,42 @@
-uncaught exception: failed to parse we get multiple states here as expected
-Watchdog error: Cannot read LSP message: Stream was closed
+{"textDocument": {"uri": "file://infoIssues.lean"},
+ "position": {"line": 3, "character": 2}}
+{"rendered":
+ "```lean\nx y : Nat\nh : x = y\nthis : y = x\n⊢ 0 + x = y + 0\n```",
+ "goals": ["x y : Nat\nh : x = y\nthis : y = x\n⊢ 0 + x = y + 0"]}
+{"textDocument": {"uri": "file://infoIssues.lean"},
+ "position": {"line": 13, "character": 33}}
+{"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```\n---\n```lean\np : Prop\nn✝ : Nat\n⊢ Nat.succ n✝ = 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✝",
+  "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✝"]}
+{"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)"]}
+{"textDocument": {"uri": "file://infoIssues.lean"},
+ "position": {"line": 25, "character": 9}}
+{"rendered":
+ "```lean\ncase left\np : Prop\nx : Nat\n⊢ x = 0 + (0 + (0 + x))\n```\n---\n```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```",
+ "goals":
+ ["case left\np : Prop\nx : Nat\n⊢ x = 0 + (0 + (0 + x))",
+  "case right\np : Prop\nx : Nat\n⊢ p"]}
+{"textDocument": {"uri": "file://infoIssues.lean"},
+ "position": {"line": 27, "character": 2}}
+{"rendered": "```lean\ncase right\np : Prop\nx : Nat\n⊢ p\n```",
+ "goals": ["case right\np : Prop\nx : Nat\n⊢ p"]}