[Backport releases/v4.34.0] fix: restore trailing whitespace of nested tactic blocks in the info tree

src/Lean/Elab/InfoTree/Basic.lean

@@ -196,12 +196,12 @@ partial def InfoTree.addTrailing? (trailing : Substring.Raw) : Elab.InfoTree →
   | .node info children => Id.run do
     let stx? := info.stx.addTrailing? trailing
     -- NOTE: we need to visit the children even if `stx` was not actually changed as info trees are
-    -- not necessarily properly nested regarding syntax ranges!
-    let childTrailing := (stx?.getD info.stx).getTrailing?.getD trailing
+    -- not necessarily properly nested regarding syntax ranges! In particular, a child may end at
+    -- `trailing` even if `stx` ends elsewhere, so always pass down `trailing` itself.
     let mut changed := false
     let mut newChildren := children
     for c in children, i in 0...* do
-      if let some c' := c.addTrailing? childTrailing then
+      if let some c' := c.addTrailing? trailing then
         changed := true
         newChildren := newChildren.set i c'
     if stx?.isNone && !changed then

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -134,7 +134,12 @@ where
         -- New trees are not guarded by a transformation here so add back trailing eagerly. Unlikely
         -- to be a bottleneck but could be optimized by adding a transformation node to `InfoTree`.
         let trailing := untrimmedTac.getTrailing?.getD default
-        modifyInfoState fun s => { s with trees := trees ++ s.trees.map (·.addTrailing trailing) }
+        unless trailing.isEmpty do
+          -- Substitute info holes first so that term-level tactic blocks ending in the same token
+          -- as `tac` (e.g. `exact foo <| by ...`) regain the trailing whitespace as well.
+          modifyInfoState fun s => { s with
+            trees := s.trees.map (·.substitute s.assignment |>.addTrailing trailing) }
+        modifyInfoState fun s => { s with trees := trees ++ s.trees }
 
       withTheReader Term.Context ({ · with tacSnap? := some {
         new := next

tests/server_interactive/15053.lean

@@ -0,0 +1,78 @@
+/-!
+Regression tests for #15053: on the line after the last tactic of a nested tactic block that ends
+an incremental tactic step (e.g. an empty `·` bullet inside `have ... := by`), the goal view must
+show the nested block's goal, not the state after the enclosing tactic. The nested nodes used to
+lose the trailing whitespace trimmed for incremental reuse.
+-/
+
+-- Issue example 1: empty `·` inside a nested `by`; expected `⊢ B` right after `·` (col 5) and on
+-- the next line at cols 7 and 5; the outer state is shown at col 3 (dedented relative to `·`) and
+-- at cols 0 and 2 (the `have` column).
+example (A B C : Prop) (hA : A) : A ↔ C := by
+  have hAB : A ∧ B := by
+    constructor
+    · assumption
+    ·
+   --^ $/lean/plainGoal
+      -- cursor here
+     --^ $/lean/plainGoal
+   --^ $/lean/plainGoal
+ --^ $/lean/plainGoal
+--⬑ $/lean/plainGoal
+
+-- Same, but with a following outer tactic
+example (A B C : Prop) (hA : A) : A ↔ C := by
+  have hAB : A ∧ B := by
+    constructor
+    · assumption
+    ·
+      -- cursor here
+     --^ $/lean/plainGoal
+   --^ $/lean/plainGoal
+  sorry
+
+-- Control: empty `·` directly in the top-level block; expected `⊢ B` at cols 3, 4 and 2
+example (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
+  constructor
+  · assumption
+  ·
+ --^ $/lean/plainGoal
+    -- cursor here
+   --^ $/lean/plainGoal
+ --^ $/lean/plainGoal
+
+-- Non-empty nested blocks are affected as well: the last nested tactic must still own the
+-- following lines at its own column or deeper.
+example (A B C : Prop) (hA : A) (hB : B) : A ↔ C := by
+  have hAB : A ∧ B := by
+    constructor
+    · assumption
+    · skip
+      -- cursor here
+     --^ $/lean/plainGoal
+   --^ $/lean/plainGoal
+ --^ $/lean/plainGoal
+
+example : False := by
+  have : True := by
+    skip
+    -- cursor here
+   --^ $/lean/plainGoal
+ --^ $/lean/plainGoal
+  sorry
+
+-- Term-level nested `by` ending the tactic step
+example : True := by
+  exact id <| by
+    skip
+    -- cursor here
+   --^ $/lean/plainGoal
+
+-- Nested `by` that does not end the tactic step (unaffected)
+example : True ∧ True := by
+  refine ⟨?_, by
+    skip
+    -- cursor here
+   --^ $/lean/plainGoal
+    ⟩
+  trivial

tests/server_interactive/15053.lean.out.expected

@@ -0,0 +1,64 @@
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 14, "character": 5}}
+{"rendered": "```lean\ncase right\nA B C : Prop\nhA : A\n⊢ B\n```",
+ "goals": ["case right\nA B C : Prop\nhA : A\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 16, "character": 7}}
+{"rendered": "```lean\ncase right\nA B C : Prop\nhA : A\n⊢ B\n```",
+ "goals": ["case right\nA B C : Prop\nhA : A\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 16, "character": 5}}
+{"rendered": "```lean\ncase right\nA B C : Prop\nhA : A\n⊢ B\n```",
+ "goals": ["case right\nA B C : Prop\nhA : A\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 16, "character": 3}}
+{"rendered": "```lean\nA B C : Prop\nhA : A\nhAB : A ∧ B\n⊢ A ↔ C\n```",
+ "goals": ["A B C : Prop\nhA : A\nhAB : A ∧ B\n⊢ A ↔ C"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 16, "character": 0}}
+{"rendered": "```lean\nA B C : Prop\nhA : A\nhAB : A ∧ B\n⊢ A ↔ C\n```",
+ "goals": ["A B C : Prop\nhA : A\nhAB : A ∧ B\n⊢ A ↔ C"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 28, "character": 7}}
+{"rendered": "```lean\ncase right\nA B C : Prop\nhA : A\n⊢ B\n```",
+ "goals": ["case right\nA B C : Prop\nhA : A\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 28, "character": 5}}
+{"rendered": "```lean\ncase right\nA B C : Prop\nhA : A\n⊢ B\n```",
+ "goals": ["case right\nA B C : Prop\nhA : A\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 37, "character": 3}}
+{"rendered": "```lean\ncase right\nA B : Prop\nhA : A\nhB : B\n⊢ B\n```",
+ "goals": ["case right\nA B : Prop\nhA : A\nhB : B\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 39, "character": 5}}
+{"rendered": "```lean\ncase right\nA B : Prop\nhA : A\nhB : B\n⊢ B\n```",
+ "goals": ["case right\nA B : Prop\nhA : A\nhB : B\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 39, "character": 3}}
+{"rendered": "```lean\ncase right\nA B : Prop\nhA : A\nhB : B\n⊢ B\n```",
+ "goals": ["case right\nA B : Prop\nhA : A\nhB : B\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 50, "character": 7}}
+{"rendered": "```lean\ncase right\nA B C : Prop\nhA : A\nhB : B\n⊢ B\n```",
+ "goals": ["case right\nA B C : Prop\nhA : A\nhB : B\n⊢ B"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 50, "character": 5}}
+{"rendered": "no goals", "goals": []}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 50, "character": 3}}
+{"rendered": "```lean\nA B C : Prop\nhA : A\nhB : B\nhAB : A ∧ B\n⊢ A ↔ C\n```",
+ "goals": ["A B C : Prop\nhA : A\nhB : B\nhAB : A ∧ B\n⊢ A ↔ C"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 58, "character": 5}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 58, "character": 3}}
+{"rendered": "```lean\nthis : True\n⊢ False\n```",
+ "goals": ["this : True\n⊢ False"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 67, "character": 5}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///15053.lean"},
+ "position": {"line": 74, "character": 5}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}