Overzealous caching of tactic state

Description

In the following code snippet, applying the code action modifies the goal but the tactic state remains unchanged.

import Batteries.CodeAction

open Lean Elab Server Lsp RequestM
open Batteries.CodeAction

def rwAddCommQuickFix (tac : Syntax) : RequestM (Array LazyCodeAction) := do
  let some range := tac.getRange? | return #[]
  let doc ← readDoc
  let eager : Lsp.CodeAction := {
    title := "Replace with `rw [Nat.add_comm, Nat.one_add]`"
    kind? := "quickfix"
    edit? := some <| .ofTextEdit doc.versionedIdentifier {
      range := doc.meta.text.utf8RangeToLspRange range
      newText := "rw [Nat.add_comm, Nat.one_add]"
    }
  }
  return #[{ eager }]

@[tactic_code_action]
def codeAct : TacticSeqCodeAction := fun _params _snap _ctx i stack _goals => do
  if i == 0 then return #[]
  let (seq, _) :: _ := stack | return #[]
  rwAddCommQuickFix seq[2 * (i - 1)]

example (n : Nat) : n = n + 1 := by
  rw [Nat.add_comm]
  -- place cursor here

Context

Identified by @JovanGerb.

Steps to Reproduce

1. Place cursor at the beginning of the line below the line rw [Nat.add_comm].
2. Apply code action.
3. Tactic state remains unchanged.
4. Move cursor left or right - tactic state is updated.

Expected behavior: Tactic state is refreshed.

Actual behavior: It is not refreshed.

Versions

Lean playground (also reproduces in VS Code)
Lean 4.31.0-rc2
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the issue in the Lean playground or VS Code using the provided tactic code action example, then trace the extension's tactic-state refresh handling after a code action is applied. Done means the tactic state updates immediately without requiring cursor movement.