Overzealous caching of tactic state

[Vtec234]

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.

[Vtec234]

In InfoAux, we re-fetch the tactic state whenever one of the following deps change:

vscode-lean4/lean4-infoview/src/infoview/info.tsx

Line 606 in 17d1d08

[updaterTick, pos.uri, pos.line, pos.character, rpcSess, serverIsProcessing, lspDiagsHere],

The trouble is that when an edit is made programmatically (as in the code action) above the cursor position, none of the deps change. The simplest fix would be to subscribe to textDocument/didChange and, if the change is above the current position, bump updaterTick. But InfoAux is already insanely complex, maybe we should rewrite it to handle this in some more principled way..