)]}'
{
  "commit": "4481b1819cf56b63cddbbf263647dfa650578afd",
  "tree": "065221d1b663a7ca330c3545b7d9960e8df87830",
  "parents": [
    "c155094f54eab345cca3da867dbd888a34fbf0d2"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Wed Sep 09 12:54:39 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Wed Sep 09 12:56:03 2026 +0000"
  },
  "message": "fix: restore trailing whitespace of nested tactic blocks in the info tree\n\nThis PR fixes the goal view showing the state after the enclosing tactic instead of the nested block\u0027s goal on the line after the last tactic of a nested `have ... :\u003d by` block or `·` bullet, e.g. after an empty `·` where the next tactic is about to be typed (#15053).\n\nTactic steps are elaborated without the trailing whitespace of their last token for incremental reuse (#11958), which is re-added to the resulting info trees afterwards. `InfoTree.addTrailing?` passed each node\u0027s own trailing whitespace to its children instead of the trailing being added, which cut off propagation at the `by` token node that `have ... :\u003d by tacs` expands to via `with_annotate_state`, so the last nested tactic never regained its whitespace. Term-level blocks ending a tactic step additionally hide behind an unsubstituted info hole at that point, so `evalSepTactics` now substitutes holes before re-adding.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\nClaude-Session: https://claude.ai/code/session_01UUFnG7QzKo9chq1i9qDkaR\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "fc9939bf4f87681d61fccf96c734ace220ab861f",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/InfoTree/Basic.lean",
      "new_id": "07de1215431560950725f14a6d42ad9e6d39a277",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/InfoTree/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "5e1a437ad10886126355bd30ff4a3627494e06e8",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/BuiltinTactic.lean",
      "new_id": "d9c4ce60d1060de505789cfdb0c71a1d98dcee8a",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/BuiltinTactic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "1c940cbe6968c0ff0b6e15ab0dc39e5a6739c456",
      "new_mode": 33188,
      "new_path": "tests/server_interactive/15053.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "75be4cd4f9aa79e60a6411e6b1b3af9f62f3170a",
      "new_mode": 33188,
      "new_path": "tests/server_interactive/15053.lean.out.expected"
    }
  ]
}