Skip to content

fix(selection): end a held selection when its file changes while you are in the Claude terminal - #481

Merged
ThomasK33 merged 15 commits into
mainfrom
fix/selection-held-buffer-changed
Nov 11, 2026
Merged

ThomasK33 merged 15 commits into
mainfrom
fix/selection-held-buffer-changed

Conversation

@ThomasK33

@ThomasK33 ThomasK33 commented Nov 10, 2026 •

Copy link
Copy Markdown
Member

What Claude holds is what you see, one case more

Claude keeps the text you selected after a file changes under it, as long as you stay in the Claude terminal. You select alpha, press Esc, go to the Claude terminal and ask a question. Claude rewrites the file on disk, Neovim reloads it (autoread, :checktime, or a focus change), and getCurrentSelection still answers alpha for a file that no longer has it. The same happens when a plugin edits the file. Coming back to the file heals it. Until then Claude answers about text that is gone.

This PR ends the hold in that case: Claude gets the cursor of the file, in the window where you left it.

Why #452 missed it

A selection survives a visit to the Claude terminal (issue #246), and nothing updates the selection while the terminal is current. #452 ends the hold when the held text changes, but it checks that from TextChanged and BufEnter. TextChanged fires only for the current buffer, and a reload or a plugin edit of the file does not fire BufEnter either. demote_if_selection_text_changed also returned when the selection's buffer was not the current one. The verify-selection-tracking model (#477) had no step that edits a buffer that is not current, so it could not see this. A reviewer of #477 found it.

The fix (lua/claudecode/selection.lua)

  1. Each time a visual selection is read (record_selection_read, in the flush and in the in-visual update), the plugin also attaches a listener to that buffer with nvim_buf_attach (on_lines, on_reload, on_detach). It is attached once per buffer: watched_buffers records it, and the entry is cleared only when the listener detaches (on_lines returns true, or Neovim calls on_detach). The exception is a module reload without disable(): the old module's listener stays on the buffer, and the new module attaches its own.
  2. The listener detaches itself at the next on_lines after Claude no longer holds a selection of that buffer (the callback returns true). While it is attached, one change, or a burst of them (:%s), schedules one check.
  3. demote_if_selection_text_changed now also runs when the Claude terminal is current and the selection's buffer is another one: if the changedtick moved and the held text is no longer at its range, it clears the held state and sends the cursor of that buffer. update_selection cannot do that, because it does nothing in the Claude terminal. The cursor is where a window shows the buffer. A buffer in no window gets the position where you released the selection, kept inside the text that is there now.
  4. :edit and :edit! detach the listener (Neovim calls on_detach), so on_detach attaches it again from a vim.schedule callback when the buffer still holds the selection, and checks it at once. A synchronous re-attach inside on_detach makes Neovim loop for ever, because it detaches the listener that was just attached. :checktime and autoread keep the listener and call on_reload, whose return value Neovim ignores, so only on_lines can detach it. on_detach also fires for :bdelete, :bunload and :bwipeout. An unloaded buffer is left alone: nvim_buf_attach returns false for it, and a watched_buffers entry set before that would stay set and block the next listener after the buffer loads again.
  5. update_selection runs the same check when the Claude terminal is current, before it returns. A new Claude terminal is not registered when BufEnter fires, so a file that changed while you were in another file, just before you opened the terminal, finds the check false at BufEnter. The 100 ms debounce is the first event that knows the terminal. The verify-selection-tracking model (feat(skills): add verify-selection-tracking, a TLA+ model of selection tracking #477) found this combination. On real Neovim the terminal's own events happen to run the check in the cases I replayed, so I could not show a stale selection there, and I did not want the fix to depend on those events.
  6. When no window shows the buffer, the fallback cursor goes through code_point_start, so a byte column that falls inside a multibyte character moves to its first byte (db3b731, Codex round 3).

cursor_selection is the table that M.get_cursor_position built, moved into a helper so the new code can build one for a buffer that is not current.

Entering the terminal, a :w, an edit that leaves the held text in place, and a reload that leaves it in place all keep the selection, as before. The listener runs in the file's buffer, not only while the terminal is current. For the current buffer it is the same check as TextChanged, a moment earlier.

Proof

Probes on real Neovim 0.12.3, through the real start() path with real timers, on origin/main and on this branch:

Path (Claude holds alpha in a.txt, you are in the Claude terminal) main this PR
a plugin deletes alpha (nvim_buf_set_text), a.txt is in no window BUG Claude holds "alpha", a.txt is "beta gamma" OK, Claude holds the cursor at 0:4
Claude rewrites a.txt on disk, :checktime reloads it, a.txt stays in its own window BUG Claude holds "alpha", a.txt is "beta gamma" OK, Claude holds the cursor at 0:4

Tests. All five new integration cases and 14 of the 19 new unit cases fail on origin/main's selection.lua and pass here. Five unit cases pass on main too, because they check that something does not happen: "keeps the selection when the change leaves its text in place", "does not send a cursor while you are in another file", "does not read a buffer that was unloaded while you stay in the terminal", "does not read a buffer that was unloaded", and "stops listening when tracking is disabled".

  • tests/integration/selection_held_spec.lua (real Neovim): five new cases. A plugin edit with the file in no window, a reload with the file in its own window, a reload that leaves the text in place (the selection stays, and the next change is seen), :bunload! then :buffer then a new selection then a plugin edit (a new listener is attached), and three select-and-reload cycles that must attach one listener, not three. All five fail on origin/main's selection.lua and pass here, on Neovim 0.12.3 and on v0.8.0.
  • tests/selection_test.lua: 19 new cases for the listener: attached once, the cursor from the window, the position kept inside the text and on the first byte of a multibyte character (db3b731), :edit! that detaches the listener, :checktime that keeps it (on_reload), one listener after a reload while only a cursor is held, a buffer unloaded and loaded again, a change that leaves the text in place, the current buffer and another file left alone, a burst checked once, detaching when nothing is held or tracking is off, and the debounce check for a terminal that was not registered at BufEnter. The mock of nvim_buf_attach now behaves like Neovim: it keeps a listener after on_reload whatever the callback returns, returns false for an unloaded buffer, and calls on_detach while the other listeners are still attached (a listener attached from inside on_detach is detached in turn, and a loop is cut after 20 calls), with vim.schedule running later.
  • Mutants. My own check: 14 mutants of the new code (no listener, never detach, clear before reading the position, no unloaded guard in the check, no re-attach, no dedupe, no window cursor, terminal not required, no row clamp, no multibyte snap, on_reload forgets its buffer, on_reload does nothing, no nvim_buf_is_loaded in on_detach, re-attach in on_detach without vim.schedule). The unit tests kill all 14. The root's verifier also ran mutants of the code at 62a11e4 (27, six survived) and at e97f6f3. What survived and what I did:
    • the nvim_buf_is_loaded guard in on_detach (it brought the bug back after :bunload!, :buffer, a new selection, the terminal and a plugin edit): killed by a unit case and a real-Neovim case, and by a mock that returns false for an unloaded buffer. The guard in demote_if_selection_text_changed has its own case.
    • the re-attach in on_detach without vim.schedule (Neovim loops for ever on :edit! or :bunload! of a held buffer): killed by the on_detach mock above. The :edit! cases fail with "on_detach loops".
    • M19, a listener that stays on a.txt after the hold moves to b.txt: declined, Claude holds the same text. M24 and four others: judged equivalent, no sequence of keys reaches a different result.
  • mise run format-check and mise run check pass. My changes add no luacheck warning: selection.lua and the integration spec have 0, and tests/selection_test.lua has the one that origin/main has. mise run test: 1341 successes, 0 failures, 0 errors.
  • .agents/skills/verify-diff-lifecycle/covered.lock is re-recorded: only the hash of selection.lua changed, and that skill covers no selection code.

Docs

ARCHITECTURE.md, README.md (global side effects), lua/claudecode/README.md (side effects), CLAUDE.md and .agents/skills/verify-claudecode-nvim/features/selection.md say that a change to the selected text while you are in the Claude terminal sends the cursor of its file, and that the plugin attaches nvim_buf_attach listeners to the buffer of a held selection.

Review record

Codex rounds on exact heads: 7033002 clean, 62a11e4 clean, beb43ee one P2 (a fallback cursor inside a multibyte character, fixed in db3b731), e97f6f3 clean, 7f48a9d clean, 117afc4 clean. Six rounds, the limit.

The root's verifier ran three times:

  1. On 62a11e4: the on_reload leak, the false comments about reloads and the feature doc wording (fixed in beb43ee), and an untested nvim_buf_is_loaded guard in on_detach.
  2. On e97f6f3: the same untested guard (fixed with its unit and real-Neovim cases in 6eba6a5), the side-effect lists in README.md, lua/claudecode/README.md and CLAUDE.md (also 6eba6a5), and N1: a synchronous re-attach in on_detach makes Neovim loop for ever, and no test failed on that mutant. The on_detach mock now matches Neovim and a case fails on that mutant (117afc4). 7f48a9d added the real-Neovim case for one listener per buffer through reloads.
  3. On 7f48a9d: PASS. It carries to 117afc4, which changes tests only.

Declined with a reason: re-reading the held range on every change (main pays the same cost through TextChanged when the buffer is current), and mutants M19 and M24.

Left as follow-ups, not fixed here:

  • A module reload without disable(): the old module's listener outlives its next on_lines for as long as the old module still holds a selection, and it can send a cursor that replaces the new module's selection. It needs a module reload, which a user does not do.
  • With nohidden, a file that is unloaded while you are in the terminal and then changes on disk is not seen until you return to it, because Neovim does not see that change either.

Follow-up

The verify-selection-tracking model (#477) gets a step for an edit of a buffer that is not current once this merges, so NoDeletedText covers it.


Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Nov 10, 2026 •

Copy link
Copy Markdown
Codex Review Summary: ✅ Completed

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-11-11T02:01:20.672800Z 117afc4 Manual request
🔒 Security Review ✅ Completed 2026-11-11T02:02:10.768631Z 117afc4 Manual request
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Keep them coming!

Reviewed commit: 703300211e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 703300211e

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 62a11e4b86

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. 👍

Reviewed commit: 62a11e4b86

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Neovim ignores what on_reload returns, so a listener that cleared its watched_buffers entry
there stayed attached and the next read attached a second one. Only on_lines detaches now.
An independent review found it. Also: say which reloads detach the listener (:edit, :edit!)
and which keep it (:checktime, autoread), fix the test mock to match, and narrow the
feature doc: the cursor goes out when the selected text changes or moves.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: beb43ee7a3

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: beb43ee7a3

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread lua/claudecode/selection.lua Resolved
…yte character

Codex round 3 (P2): when no window shows the selection's buffer, the release position is kept
inside the new text, and its byte column can fall inside a multibyte character. Snap it with
code_point_start, which moves up next to the code that uses it first.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: e97f6f37dd

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: e97f6f37dd

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Can't wait for the next one!

Reviewed commit: 7f48a9da23

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 7f48a9da23

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex review

@ThomasK33

Copy link
Copy Markdown
Member Author

@codex security review

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Nice work!

Reviewed commit: 117afc45b8

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@chatgpt-codex-connector

Copy link
Copy Markdown

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 117afc45b8

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

  • You comment "@codex security review"
  • A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

@ThomasK33
ThomasK33 added this pull request to the merge queue Nov 11, 2026
Merged via the queue into main with commit d34a830 Nov 11, 2026
8 checks passed
@ThomasK33
ThomasK33 deleted the fix/selection-held-buffer-changed branch November 11, 2026 03:24
ThomasK33 added a commit that referenced this pull request Nov 11, 2026
…-selection-tracking

The model gets a YouEditOtherBuffer step (a reload or a plugin edit of a file that is not the
current buffer: no TextChanged, no BufEnter) and three facts, ListensToSelectionBuffer,
TerminalReportsHeldBuffer and UpdateChecksHeldText, for the guards that #481 added to
selection.lua. NoDeletedText covers the path now. FlushSkipReports breaks no rule alone any
more, because the terminal's debounce check finds the stale text: it is caught with
EntryClearsHeld. NoDeletedText runs with two files in --mutants. Two replays, a reload and a
plugin edit while you are in the Claude terminal, are red on main before #481.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
ThomasK33 added a commit that referenced this pull request Nov 11, 2026
The merge brings in #481, which changes the selection code and its docs.

_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
hareki pushed a commit to hareki/claudecode.nvim that referenced this pull request Nov 12, 2026
…s a closed diff leaves (coder#491)

## Why

A user who switches a diff's window to another file (`:edit other.txt`)
and then sets something of its own in that window lost it when Claude
called `close_tab`. Two things were overwritten:

- In the unified layout, the sign column. The cleanup added in coder#483
wrote the value from before the diff back (`:setlocal signcolumn=yes:2`
became `auto`).
- In the split layout, diff mode. The cleanup ran `:diffoff` in every
window it kept, so a `:diffthis` or `:setlocal diff` that the user ran
after the `:edit` ended at `close_tab`. Main has this too.

## What changed

- `diff_inline.lua` sets `'signcolumn'` to `yes` with `scope = "local"`,
like `:setlocal`. `nvim_set_option_value(..., { win = ... })` behaves
like `:set` and also sets the window's default, which every buffer shown
there later inherits. coder#483 hid that by restoring the old value
unconditionally, and that restore overwrote the user's choice. With
local scope the window shows `yes` for the proposal buffer only, a
window that the user switches shows the sign column it had before the
diff, and a value the user sets there stays. The cleanup has nothing
left to restore, so the saved value is gone from the diff record.
- `diff.lua`: the split layout's cleanup runs `:diffoff` in a kept
window only while that window still shows the file's own buffer. `:edit`
to another buffer already turns diff mode off, unless the new buffer is
in diff mode in another window, as the file's own buffer is (`:edit #`).
So a diff mode in a window that shows another buffer is the user's and
stays. Both kept windows follow this rule: the proposal window and the
original-side window. The proposal window's `:diffoff` moves into the
split-only branch of `_cleanup_diff_state`, so the unified layout cannot
reach it.
- The journey script gets a step for the user's own sign column, and its
header names it. A stale comment about the sign column is gone. The
journey line in `SKILL.md` names every command the journey runs,
including `:b hello.txt`, except the `:only` resets between steps. The
README claim about the cleanup is updated and cites `setup_inline_diff`.
- `covered.lock` is re-recorded. The changed code is one window-option
call in `setup_inline_diff` and the window-handling lines of
`_cleanup_diff_state` and `_close_proposal_window`. None of it touches
how a diff is resolved, closed or answered, and `check.sh` passes.

### Why not "restore only while the window still shows `yes`"

I tried that first for the sign column. It passes the headless spec and
fails in a live session. When `:edit` or `:b` already gave the window
its own value back, the guard skipped the restore and left the window
default at `yes`, so the next `:edit third.txt` in that window showed a
sign column again. The journey run caught it. Local scope fixes both
cases, and the added spec case checks both.

### The split layout

The split layout sets window options with `:diffthis` (`diff`,
`scrollbind`, `cursorbind`, `wrap`, `foldmethod`, `foldcolumn`,
`foldenable`, `foldlevel`). I checked each one in the proposal window
and in the original-file window: `:edit` another file, set the option,
then `close_tab`. Seven of them keep the user's value on Neovim 0.12.3
and v0.8.0 (14 checks per version, 0 failures). Neovim restores these in
`:diffoff` only when the buffer was put in diff mode in that window, and
`:edit` clears that state. `'diff'` itself is different: `:diffoff`
always turns it off, which is why the cleanup now runs it only where the
diff left diff mode on.

One limit stays, and it is Neovim's own. With the default `diffopt` (it
contains `closeoff`), when a window in diff mode closes and exactly one
window in diff mode is left, Neovim turns diff mode off in that window.
Two cases reach a user's diff mode: a kept original-side window when the
proposal window closes, and a kept proposal window when the cleanup
closes the window that the plugin opened for the file (the current
window showed another file), including the fallback window it opens when
no editor window fits. A user's diff mode over two or more windows
stays. With `closeoff` removed from `diffopt`, a lone window stays too,
in both cases (checked on Neovim 0.12.3 and v0.8.0).

## Evidence

Before this PR, on the coder#483 merge commit:
- The new sign column spec case fails in 5 of 73 cases (unified layout:
the window shows `no` where the user set `yes:2`).
- The real-Neovim journey (`journey-diff-close-save.sh`, unified layout,
existing file) fails its new check: 1 of 23.

On current main, this head's `diff_close_save_spec.lua` fails 7 of 77
cases: 5 sign column cases in the unified layout and 2 diff mode cases
in the split layout.

After, on this head:
- Spec (`diff_close_save_spec.lua`): 77 pass on Neovim 0.12.3, 40 pass
on v0.8.0 (the unified layout skips below 0.9).
- Journey: PASS 23 of 23 in all four runs (unified and split, existing
and new file).
- `mise run all`: exit 0, 1341 successes, 0 failures, 16 pending (after
the merge of coder#481). The integration runner passes 254 cases on 0.12.3
and 171 on v0.8.0, with the stub `claude` first on PATH. The runner's
own "Total Success" line adds one summary line per file, so it reads 272
and 189.
- The new diff-mode cases fail on the previous head (2 of 77: the split
layout's proposal window and original-side window) and pass on this one.

Mutants, each turns the named spec case red:
- Dropping `scope = "local"`: 10 cases (both "keeps the 'signcolumn'..."
groups).
- Restoring coder#483's unconditional restore: the "keeps the 'signcolumn'
that the user set" case.
- Dropping the "still shows the file's own buffer" check for the
proposal window: "keeps the diff mode ... proposal window that :edit
switched in the vertical layout".
- Dropping the same check for the original-side window: "keeps the diff
mode ... original-side window that :edit switched in the vertical
layout".
- Removing the proposal window's `:diffoff`: "turns off diff mode in a
proposal window that :edit # switched back to the file".
- Removing the original-side window's `:diffoff`: "does not close the
reused target window when the old file is already open" (unit spec).
- Adding an unconditional `:diffoff` of the kept window to
`_close_proposal_window`, which both layouts call: the two unified cases
"keeps the diff mode ... proposal window that :edit switched" and "...
that :edit # switched back", plus the vertical one.

Refs coder#483

---
_Generated with [`xum`](https://github.com/coder/xum) • Model:
`anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki pushed a commit to hareki/claudecode.nvim that referenced this pull request Nov 12, 2026
…eld buffer becomes a Claude terminal (coder#493)

## A held selection's buffer becomes a Claude terminal

When the buffer of a held selection becomes a Claude terminal after the
selection was read, and its text changes, two things went wrong. Neovim
raised `stack overflow` from `CursorMoved`, `TextChanged` and
`vim.schedule` callbacks, and a cursor of the terminal buffer, with a
`term://...` path, could reach Claude. This PR fixes both. It is a
follow-up to coder#481, found by the review of that PR and by the verifier of
this one.

Claude must never get a selection or a cursor of a Claude terminal
buffer: its text is Claude's own prompt. The flush and
`update_selection` ignore such a buffer, and this PR makes the held-text
check from coder#481 do the same.

## How it happens

A buffer becomes the Claude terminal after a selection was read in it
with `termopen()`, or with a rename to a `term://...claude` name. The
held-text check (`demote_if_selection_text_changed`, added in coder#481) then
runs on a buffer that is a terminal:

1. **Recursion.** `update_selection` does nothing in the Claude
terminal, except that since coder#481 it calls the check there. The check
ended every selection in the current buffer with `M.update_selection()`.
If the current buffer is the terminal and also the buffer of the
selection, the two functions call each other until the stack overflows.
The reviewer of coder#481 reproduced this with the rename, and I did the same
on real Neovim 0.12.3. A custom `terminal_cmd` after a plugin reload did
not reproduce it: the native provider adopts the old terminal at the
first terminal check.
2. **A pending demotion.** If the demotion timer is pending when the
buffer becomes the terminal, it fires later and takes the buffer for an
ordinary one: `handle_selection_demotion` knows only the terminal that
the provider registered. It then sends the cursor of the terminal buffer
(found by Codex in round 2, confirmed by the verifier).
3. **Another Claude terminal.** You are in a Claude terminal and the
buffer of the held selection becomes a Claude terminal too. The check
took it for a file and sent its cursor, with a `term://...` path. This
path exists on `main` since coder#481 (found by the verifier).

## The fix (`lua/claudecode/selection.lua`)

In `demote_if_selection_text_changed`, one branch handles a held buffer
that is a Claude terminal while you are in a Claude terminal (the same
one, or another):
- It calls `M.update_selection()` only when the current buffer is not a
Claude terminal, so the two functions cannot call each other.
- It clears the held state (`cursor_at_flush`,
`last_active_visual_selection`), as before.
- It cancels a pending demotion (`M._cancel_demotion_timer()`).
- It forgets the read of the selection (`selection_tick`), so nothing
checks that buffer again and its listener detaches at its next change.
- It sends no cursor. `cursor_in_other_buffer` is called only for a held
buffer that is not a Claude terminal, which is the coder#481 case that stays
as it was.

Claude keeps the selection it already has: nothing in this branch
replaces `latest_selection`.

## Proof

- Real Neovim 0.12.3, through the real `start()` path: select `alpha`,
press Esc, rename the buffer to `term://x//1:claude`, delete `alpha `
with `nvim_buf_set_text`. On `origin/main`: `Error in CursorMoved
Autocommands`, `Error in TextChanged Autocommands`, and `Lua callback:
stack overflow` in `v:errmsg`. With the fix: no error, and no broadcast.
- `tests/selection_test.lua` (3 cases for this PR): no recursion, a
pending demotion is cancelled, and nothing is sent when you are in
another Claude terminal. Each asserts that nothing was broadcast and
that `get_latest_selection()` still returns the held selection
(`alpha`). The recursion case also asserts the held state is gone, the
read is forgotten and the listener detaches at its next change. The case
for path 3 is red on the previous head (it sends the `term://` cursor).
A mutant that also clears `latest_selection` in the new branch fails all
three.
- `tests/integration/selection_held_spec.lua` (real Neovim, 3 cases):
the same three paths. Each records every `selection_changed` broadcast
and asserts that none was sent and that `get_latest_selection()` is
still `alpha`. The first and third also assert that the read is
forgotten, and the first also asserts that `v:errmsg` stays empty. The
case for path 3 is red on the previous head. The whole spec passes on
Neovim 0.12.3 and v0.8.0 (14 of 14).
- `mise run format-check`, `check` and `test`: 1344 successes, 0
failures. `selection.lua` and the integration spec have 0 luacheck
warnings, and `tests/selection_test.lua` has the one that `origin/main`
has.
- `.agents/skills/verify-diff-lifecycle/covered.lock` is re-recorded:
only the hash of `selection.lua` changed.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model:
`anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki pushed a commit to hareki/claudecode.nvim that referenced this pull request Nov 12, 2026
… edits another line or writes the file (coder#524)

## Result

Claude gets the selection you released, not the cursor, when a plugin
edits another line or the file is written while you are in visual mode.
This holds for a quick release (within the 100 ms debounce) and for a
slow one.

Before: `ve`, then a plugin edits line 2, then `Esc` within 100 ms.
Claude got the cursor (`a.txt "" 0:4-0:4`). After: Claude holds `alpha`.

## Cause

`flush_visual_selection` skips the release on `Esc` when the buffer's
changedtick moved since visual mode began (the guard from coder#246). The
guard is for an operator (`d`, `c`, `>`, `gU`...) that consumes the
selection: the `'<` and `'>` marks then point at text you never
selected, so a release would send a phantom selection.

Five things move the changedtick: an operator, a plugin's edit, an undo
(from a plugin or a `<Cmd>` mapping), a `:write` of a modified buffer (5
-> 6), and a reload (`:checktime`, `:edit!`). An operator and a reload
consume the selection. The other three leave it on the screen.

## Fix

1. Neovim ends visual mode before an operator changes any text. A
plugin's edit runs while visual mode is on. A `:write` fires no buffer
callback at all.
2. `watch_selection_buffer` (the coder#481 listener on the held buffer) now
also listens to the buffer you select in. There is still one listener
per buffer. It detaches at the first edit after the selection is over,
as before, unless the buffer holds a selection.
3. `visual_entry` no longer stores a changedtick. It stores `consumed`
and `unchecked_edits`. The flush skips when `consumed` is set or an edit
is unchecked.
4. Neovim 0.8 and 0.9 end visual mode for the length of an
`nvim_buf_set_lines` or `nvim_buf_set_text` call, and run the callback
in that state (0.10 and later run it in visual mode). So the callback
only counts the edit, and `vim.schedule` reads the mode after the call.
An operator's flush comes before that check, so it finds an unchecked
edit and skips.

A reload or a detach of the buffer during visual mode counts as an
operator. The Claude terminal buffer is not listened to: its output is a
stream of edits, and the flush ignores it.

## What does not change

1. A real consuming operator still sends nothing: `d`, `c`, `>`, a
linewise `>`, and an operator after a plugin's edit or after a `:write`.
2. In-place operators (`gU`, `~`, `J`) stay skipped, as the old comment
says.
3. If a plugin's edit and `Esc` are handled in the same event-loop turn
(both are in typeahead), the check has not run, and the flush skips.
That is the old behavior, not a regression.
4. A plugin edit of the selected text or of its line keeps the release:
Claude gets the text that Neovim highlights after the edit. On Neovim
0.8 to 0.11, an earlier edit on the same line shifts the highlight, and
a plugin that inserts lines above the selection leaves the visual anchor
on its old line number. The flush sends what the editor highlights. The
new spec does not test these cases.

## Tests

| Where | What |
|---|---|
| `tests/integration/selection_visual_edit_spec.lua` (new, real Neovim)
| 12 tests. For 20 ms and 300 ms between the steps: plugin edits line 2,
plugin appends lines, `:write` of a modified buffer. Guards: `ved`,
`vec`, `Vj>`, `d` after a plugin edit, `d` after a `:write`. Next
selection does not inherit an operator. |
| `tests/selection_test.lua` | 4 operator tests now fire the buffer
listener as Neovim does. 8 new tests (plugin edit, `:write`, operator
after plugin edit, unchecked edit, reload, next selection, detach,
terminal buffer). |

Red on main: 6 of the 12 integration tests (the plugin-edit and `:write`
cases at both delays). The 6 guards pass on main.

Mutants, all killed: 2 integration (the flush never skips, every edit
counts as consumed) and 8 unit (flush never skips, unchecked edit
ignored, always consumed, never consumed, reload ignored, entry not
cleared, terminal watched, no detach).

Checked on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3: the new spec
passes 12 of 12.

Gates: `treefmt --ci` is clean and luacheck shows 0 warnings in 178
files. Busted gives 1663 unit tests passed, 0 failed, 24 pending (no
coverage). The integration runner, once normally and once under a
`TMPDIR` named `odd tmp 50%`, in a private `HOME`, passes 331 tests per
run on 0.12.3 and 244 per run on 0.8.0, with 0 failures.
`verify-diff-lifecycle/check.sh` matches after the re-record: only the
hash of `selection.lua` changed, which cannot reach diff state, and the
model passes (89,205 distinct states). The docs say what the listeners
do (`lua/claudecode/README.md` and the Global Side Effects list in
`README.md`).

## Follow-up

`verify-selection-tracking` (coder#477) models the changedtick. It gets a
separate round after this merges.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model:
`anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki pushed a commit to hareki/claudecode.nvim that referenced this pull request Nov 13, 2026
…n tracking (coder#477)

## Status

coder#524 is merged (`a41254a4`). It changed the flush on visual exit: the
changedtick comparison is gone, and a `visual_entry` that the buffer
listener marks takes its place. This PR models it. Codex round 4
(`91660323`) raised two P2 threads, fixed in round 5 (`f974ee06`: both
lanes clean). The Opus and GPT verifiers of `f974ee06` found one
documentation defect and three minors, fixed in this round 6 (the last).
The replays also found a family of bugs that coder#524 left: any edit made
while you select whose check has not run when the next key arrives.
Three are reproduced (a mapping, a key that arrives during the plugin's
callback, an autocmd edit at a mode change), and fix PR coder#540 fixes all
three. Their replays print `BUG` on `main` until coder#540 merges.

## What this adds

`.agents/skills/verify-selection-tracking/`: a TLA+ model of what Claude
sees as the user's current selection (`lua/claudecode/selection.lua`),
checked by TLC against guards that `check.sh` reads from the Lua code,
on the shared harness from coder#450. The model has no clock, so it covers
every `visual_demotion_delay_ms`. A change that removes or rewords a
guard makes a rule break or the covered code read STALE.

The model describes `main` as it is now: the four bugs it found are
fixed (coder#452), and so are the cases that reviews found afterwards (coder#471,
coder#481, and the recursion of coder#481's code that coder#493 fixed).

## The ten rules, as plain sentences

| Rule | Plain sentence |
| --- | --- |
| `ReleaseSent` | Right after you release a selection in a file (Esc),
Claude holds it, also when you made it faster than the 100 ms debounce
(issue coder#246), and when a plugin edited another line or a `:write` ran
while you selected. |
| `NoPhantomSelection` | Claude only gets text you selected, never the
text at the `'<,'>` marks after an operator such as `d` changed it. |
| `NoTerminalSelection` | Claude never gets a selection in the Claude
terminal buffer. |
| `HeldUntilMoved` | Once events settle in a file, a selection you
released stays with Claude while the cursor has not moved and its text
is unchanged. |
| `HeldInTerminal` | Once events settle in the Claude terminal, Claude
still holds the selection you released while its text is unchanged. |
| `HeldEndsWhenMoved` | Once events settle in a file, Claude holds a
released selection only while the cursor has not moved since you
released it. |
| `SameFile` | Once events settle in a file, Claude's selection is in
that file. |
| `ClaudeSeesCursor` | Once events settle in a file, a cursor-only
selection that Claude holds is where the cursor is, and in visual mode
Claude holds the live selection. |
| `NoDeletedText` | Once events settle, Claude holds no selection text
that its buffer no longer has. |
| `TimerClosedOnce` | No timer handle is closed twice (Neovim would
raise `handle ... is already closing`). |

"Once events settle" means no debounce or demotion timer runs, no timer
callback waits in the `vim.schedule` queue, and the check that the
buffer listener queued with `vim.schedule` has run.

## Bugs this model found

The first version of the model broke four rules on the code before coder#452.
Each path was replayed on Neovim 0.12.3. **coder#452 fixed all four**:

1. `HeldEndsWhenMoved`: Claude kept a released selection after the
cursor left it (`vb` Esc `gv` `d`, or `ve` Esc `l` `h` inside 100 ms).
2. `NoDeletedText`: Claude kept a held selection after you edited its
text without moving the cursor (`viw` Esc `x` `x`).
3. `SameFile`: with a long `visual_demotion_delay_ms`, Claude held
another file's cursor (`:b b.txt`, `:b a.txt`).
4. `ClaudeSeesCursor`: with a long `visual_demotion_delay_ms`, Claude
held a cursor position you had left (Esc `l`, wait, `h`).

**coder#471** closed the case a Codex review of coder#452 found: an operator
consumes a second selection and you enter the Claude terminal within the
debounce. The model's flush-skip step (`FlushSkipReports`) describes the
fixed code, and `tests/integration/selection_held_spec.lua` replays the
path with a real terminal buffer.

**coder#481** closed the case a reviewer of this PR found, and no step of the
model could express it: Claude holds selection A, you go to the Claude
terminal, and A's file changes while you are there (Claude rewrites it
and Neovim reloads it, or a plugin deletes the selected text). Claude
kept the deleted text until you came back. The model now has a step for
it (`YouEditOtherBuffer`) and three facts: `ListensToSelectionBuffer`,
`TerminalReportsHeldBuffer` and `UpdateChecksHeldText`.
`replays/held_after_reload_in_terminal.lua` and
`replays/held_after_edit_in_terminal.lua` replay the two triggers on
real Neovim.

**coder#524** closed the case an advisor of this PR found, and no step of the
model could express it: you select, a plugin edits another line (or a
`:write` runs) while you are still in visual mode, and you press Esc
inside the 100 ms debounce. The flush took a moved changedtick for an
operator that consumed the selection, so Claude got the cursor and not
the selection. The model now has two steps that move only the
changedtick (`YouEditByPluginInVisual`, `YouWriteInVisual`) and three
facts for the new code (`FlushSkipsOperator` rewritten,
`ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit`).
`FlushIgnoresTick` is the old comparison as a fact: it reads `FALSE` on
the code before coder#524, and the model then breaks `ReleaseSent` and
`HeldUntilMoved` (`NoPhantomSelection` still holds, because the old
guard did stop operators). Three replays
(`release_after_plugin_edit_in_visual.lua`,
`release_after_plugin_append_in_visual.lua`,
`release_after_write_in_visual.lua`) print `BUG` on `fcea49af` (the
commit before coder#524) and `OK` on `main`, on Neovim 0.12.3 and 0.8.0.

**Still open, found by the replays:** the flush on Esc skips a selection
that has an edit nobody checked yet, and the check that clears a
plugin's edit runs in `vim.schedule`, after the command or callback that
made the edit returns. When a key comes first, the flush takes the edit
for an operator's and Claude gets the cursor, not the selection,
although its text is untouched. The model runs that check in the step of
the edit, so it does not show this, and a PASS says nothing about it.
Three ways to get there print `BUG` on Neovim 0.8.0 and 0.12.3 (3 of 3
runs each): a mapping that edits another line and presses Esc in one
typeahead (`release_in_same_typeahead_as_plugin_edit.lua`), a key that
arrives while a timer callback of the plugin still runs
(`release_with_key_during_plugin_callback.lua`, with `nvim_input`; the
Opus verifier found it with an attached UI), and an autocmd that edits
when visual mode starts with the Esc already in the typeahead
(`release_after_autocmd_edit_in_visual.lua`, a `ModeChanged` handler for
`n:v`; the GPT verifier found it). In a tree with coder#540 (a `vim.on_key`
listener runs the check at the next key) all 16 replays print `OK` on
both versions. A plugin edit whose check runs before the next key is not
affected (`release_after_plugin_edit_in_visual.lua`).

**coder#457** and **coder#463** changed `getCurrentSelection` and moved the
terminal check into `M.is_claude_terminal_buffer`. The model follows
that move (`FlushSkipsTerminal`, `UpdateSkipsTerminal`). It makes no
claim about what `getCurrentSelection` answers when nothing is tracked.

## What changed from the model that found those bugs

- The model now describes the fixed code: `clear_held_state`,
`reconcile_held_selection` (called from `CursorMoved`, `BufEnter` and
`TextChanged`), the changedtick record `selection_tick`,
`cursor_at_flush.left` and `.away`, and the flush-skip report. That adds
nine facts (21 in all), the coder#481 guards add three (24 in all), and the
coder#524 guards add three more (27 in all).
- `SameFile` and `ClaudeSeesCursor` no longer break on the code as
written. The special case that ran their mutants with
`DelayBelowDebounce = TRUE` is gone, and the check uses `FALSE` (every
delay).
- Five guards break no rule alone, because another guard covers for them
(`FlushSkipReports` only together with `EntryClearsHeld`). `--mutants`
removes each with its partner (four `A+B` keys in `EXPECT`):
`DemotionClearsHeldState` + `MoveReports` and `PendingClearsHeld` +
`ReconcileOnCursorMoved` break `ClaudeSeesCursor`, `ElseClearsHeldState`
+ `LeaveNoted` breaks `SameFile`, `EntryClearsHeld` + `FlushSkipReports`
breaks `HeldEndsWhenMoved`. I found these pairs by running each such
guard together with each other guard. SKILL.md lists them.
- The model has a `YouEditByPlugin` step: `TextChanged` without
`CursorMoved`. In the model, `ReconcileOnTextChanged` and
`TextChangeReports` each break `NoDeletedText` alone because of it. On
real Neovim they do not: the buffer listener (`on_lines`) also fires for
an edit of the current buffer and runs the same check.
`replays/held_after_plugin_edit.lua` prints `OK` with either call
removed from `lua/` (I removed each: all 18 replay runs print `OK`,
while `check.sh` reports `BROKEN: NoDeletedText`). So a `BROKEN` trace
for these two guards is a counterexample of the model, not a failure of
the running plugin. SKILL.md says so. `--mutants` still requires both
guards, because the model has no other way to end the hold at that edit.
- The model keeps the changedtick as one bit on the visual entry ("moved
since visual mode started"), not as a number per buffer: the code before
coder#524 only compared it with the value recorded at entry, and a
changedtick only grows. A number per buffer multiplies the states and
the `--mutants` time by an estimated 5 to 10 and adds no behavior (I did
not build it). The bit is kept only while an entry exists and a guard
reads it, so the main run has fewer states (129,986) than before
(178,962).
- `LeaveNoted` breaks `HeldEndsWhenMoved` alone only when the user can
visit a second file, so `--mutants` runs that rule with two files.
- The model has a `YouEditOtherBuffer(b)` step: the text of a buffer
that is not current changes, `TextChanged` does not fire for it, and the
plugin sees the change only through its `nvim_buf_attach` listener
(`on_lines`, `on_reload`, `on_detach`) or when you come back. The
listener only queues its check with `vim.schedule`, so the model sets a
queued-check bit at the edit and runs the check in its own step
(`ListenerCheckRuns`), after any other step (Codex round 2).
`ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and
`UpdateChecksHeldText` are the guards of coder#481 that break `NoDeletedText`
when removed.
- `HeldInTerminal` is new in this round (Opus verifier).
`HeldUntilMoved` only holds in a file, so two regressions that drop a
released selection in the Claude terminal passed every rule:
`update_selection` in the terminal that reports the cursor although the
text did not change, and a demotion in the terminal that publishes the
cursor of the held buffer. The new rule says that Claude keeps the
selection there. It passes on the model, and six guard removals break
it, so it is not vacuous.
- The 16 replays (`replays/`) exit 0 on `OK` and 1 on `BUG`. Eleven
replay a path that once broke a rule and show the promise kept (the
three added for coder#524 are the plugin edit, the plugin append and the
`:write` in visual mode). `held_after_line_inserted_above.lua` (a line
inserted above a held selection makes Claude lose the selection and get
the cursor, although the text still exists) and
`v_escape_selects_one_character.lua` (a bare `v` and Esc selects the
character under the cursor, so it is a selection) show things that are
not rules. Three replay known bugs and print `BUG` until coder#540 merges
(see "Still open"). `replays/run.sh` works without GNU `timeout` (macOS)
and with a checkout path that has a space, a comma or a quote (Codex
round 2).

## Proof

All on this branch, Neovim 0.12.3, Java from mise:

- `check.sh`: `main: pass (129986 distinct states found)`, `== RESULT:
PASS` (exit 0, a fresh lock), all 27 facts `TRUE`.
- `check.sh --mutants` (4486 s, about 75 min, at a load average of 22 to
31): 26 keys (22 single guards and four `A+B` pairs), `== mutants: every
guard is caught`, no rule is vacuous (exit 0). The new facts are caught
as `EXPECT` says: `FlushSkipsOperator` and `ListenerNotesVisualEdit`
break `NoPhantomSelection`, `VisualCheckSparesPluginEdit` and
`FlushIgnoresTick` break `ReleaseSent`. The run is on `c731ebae`. Since
then the model changed only in its comments (the spec without comments
is identical, and `check.sh` still reports 129,986 states), and
`check.sh` changed in one regex and its comment (the
`ListensToSelectionBuffer` regex now reads both forms of `on_lines`, see
below). The TLC inputs of `--mutants` (model, constants, `EXPECT`, and
the fact values, which are all `TRUE` on `main`) are the same, so I did
not run it again. The verifiers ran it on `f974ee06` (Opus 5075 s, GPT
5201 s): 26 keys caught, exit 0.
- The code before coder#524: `check.sh` runs on the `selection.lua` of
`fcea49af` once two stand-in blocks (`visual_entry_of`,
`note_visual_edit`, which the old code does not have) are added at the
end of the file. Exactly four facts read `FALSE`: `FlushSkipsOperator`,
`ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit` and
`FlushIgnoresTick`. `check.sh` exits 1 with `main: BROKEN: ReleaseSent`,
the first broken rule it prints (trace: you select, a plugin edits
another line, you press Esc). TLC with that fact set breaks
`ReleaseSent` and `HeldUntilMoved` (the Opus and GPT verifiers ran it
too), `--mutants` lists `HeldInTerminal` as well for `FlushIgnoresTick`,
and `NoPhantomSelection` holds. Putting the old comparison back into the
`selection.lua` of this tree gives the same: `check.sh` exits 1,
`FlushSkipsOperator FALSE`, `FlushIgnoresTick FALSE`, `main: BROKEN:
ReleaseSent`.
- Each new guard removed alone from `selection.lua` flips only its own
fact: the flush condition (`FlushSkipsOperator`, `main: BROKEN:
NoPhantomSelection`), the `note_visual_edit(entry)` call in `on_lines`
(`ListenerNotesVisualEdit`, `NoPhantomSelection`), and the mode test of
the check (`VisualCheckSparesPluginEdit`, `ReleaseSent`).
- Scratch breaks on this tree (edit `lua/`, run, then `git checkout --
lua/` and an empty `git diff --shortstat`):
- Dropping `reconcile_held_selection(not entered_buffer)` from
`M.on_cursor_moved`: `check.sh` exits 1, `ReconcileOnCursorMoved FALSE`,
`main: BROKEN: HeldEndsWhenMoved`, and
`replays/held_after_quick_move.lua` prints `BUG the cursor moved after
the release, but Claude still holds "alpha"`.
- Making the `selection_text_is_there` test in
`demote_if_selection_text_changed` always true: `check.sh` exits 1,
`TextChangeReports FALSE`, `main: BROKEN: NoDeletedText`, and
`replays/held_after_edit.lua` prints `BUG Claude holds "alpha" at 0-5,
the buffer has "alphb" there`.
- Dropping `watch_selection_buffer(bufnr)` from `record_selection_read`:
`check.sh` exits 1, `ListensToSelectionBuffer FALSE`, `main: BROKEN:
NoDeletedText`, and `replays/held_after_reload_in_terminal.lua` prints
`BUG Claude holds "alpha", but a.txt is "beta gamma"`.
- `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`.
- Replays: 16 probes on Neovim 0.12.3 and 0.8.0, each at the default
delay and with `DELAY_MS=50` (that setting changes only the two
long-delay probes): 13 print `OK` and the three known-bug probes print
`BUG` (coder#540). On `fcea49af` the three probes for coder#524 print `BUG` on
both versions. In a tree with coder#540 (a scratch copy of the skill, not
part of this PR) all 16 print `OK` on both versions, and the two new
known-bug replays ran 4 times each on both versions with the same
result.
- At `91660323`, a script that removed each of the 24 guards from
`selection.lua` alone showed that exactly its own fact turns `FALSE`
(seven regexes read a second guard before; the Opus verifier found three
of them). The regexes of `FlushOnVisualExit`, `ReconcileOnCursorMoved`
and `ReconcileOnTextChanged` are anchored now, because a commented-out
handler call used to leave the fact `TRUE`: with each call commented out
in `selection.lua`, only its own fact reads `FALSE`. This round I did
the same by hand for the three new guards (see above), and I rewrote the
`ListensToSelectionBuffer` regex twice: in round 5 for the code after
coder#524 (`on_lines` and `on_reload` call `check_soon` inside `if
holds_selection_of(buf) then`), and in this round to read both forms (it
read `FALSE` on the `selection.lua` of `fcea49af`, which listens). It is
`TRUE` on `fcea49af` and on this head, and `FALSE` when `check_soon()`
is removed from `on_lines` or from `on_reload`, and when
`watch_selection_buffer(bufnr)` is removed from `record_selection_read`
(only its own fact in each case).
- `shfmt -i 2`, `shellcheck --exclude=SC1091,SC2016`, `stylua --check`,
`prettier --check` and `treefmt --ci` (379 files, 0 changed): clean.
`luacheck` 0 warnings in 181 files. `tests/selection_test.lua` and
`tests/unit/visual_delay_timing_spec.lua`: 156 successes, 0 failures.
This PR changes no `lua/` or `tests/` file.
- `covered.lock` is recorded last. This round the flush,
`on_mode_changed` and `watch_selection_buffer` blocks changed (coder#524),
and `visual_entry_of` and `note_visual_edit` are new blocks. The file
hashes of `init.lua` and `server/init.lua` changed with `main`. In round
6 the `on_connect` block changed too (coder#539 moved a debug log line: no
send, no timer, no selection state), and the lock is re-recorded. I
merged `origin/main` several times and read each diff of the covered
code: coder#454 (`server.broadcast` returns, mention queue), coder#481, and coder#493,
whose change in `demote_if_selection_text_changed` made the regex of
`TerminalReportsHeldBuffer` read `FALSE`. I re-pointed it and
re-recorded the lock. coder#467 and coder#491 touch no covered file of this skill.
coder#497 changed one debug log argument in the `tools/call` handler of
`server/init.lua`, and coder#499 changed the disconnect cleanup in the same
file (`on_disconnect`: a client without a handshake owns no diff, and
the cleanup waits until Neovim allows window changes). Both are outside
`M.broadcast` and the `on_connect` callback, and neither can reach the
selection state, a timer or a send, so only the file hash changed and I
re-recorded the lock.

## Run it

```bash
.agents/skills/verify-selection-tracking/check.sh            # about 1 min
.agents/skills/verify-selection-tracking/check.sh --mutants  # about 1 to 1.5 h (4486 s in the last run), after you edit the model or a fact
.agents/skills/verify-selection-tracking/check.sh --hash-only  # about 5 s, only compares covered.lock with the code
NVIM=~/.local/share/mise/installs/neovim/0.12.3/bin/nvim \
  .agents/skills/verify-selection-tracking/replays/run.sh held_after_operator.lua
```

CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock`
job, as for `verify-diff-lifecycle`.

## Review record

- Codex round 1 (`ac7f243`): clean in both lanes.
- Codex round 2 (`f91391f`): security clean. Code lane, three P2s: the
model ran the listener check atomically with the edit, `replays/run.sh`
needed GNU `timeout`, and it put raw paths into Neovim commands. All
three are fixed.
- GPT and Opus verifiers on `f91391f`: ISSUES. F1 (SKILL.md scope
omitted a held buffer that becomes a Claude terminal, now a scope
bullet) and minors F3 to F10 are applied, except F4 (six blind-spot
mutants remove a guard's effect without touching a line a fact reads:
the fact stays `TRUE`, but `covered.lock` reads STALE, so `check.sh`
exits 3, not 0). F2 and the GPT finding of the same kind stay a
disclosed limit: the model runs the buffer listener only for a buffer
that is not current, although `on_lines` also fires for an edit of the
current buffer, so a `BROKEN` trace for `ReconcileOnTextChanged` or
`TextChangeReports` is a counterexample of the model, not a failure of
the running plugin (SKILL.md, "Read the result").
- Codex round 3 (`e18a1cf`): clean in both lanes.
- GPT and Opus verifiers on `e18a1cf`: ISSUES. Opus N2 (impact: the
`HeldUntilMoved` row promised more than its rule checks, and two
regressions in the terminal passed): new rule `HeldInTerminal`, rows
fixed, `--mutants` rerun. GPT F1 (impact: SKILL.md said a bare `v` and
Esc keeps the held selection, but Claude gets the one selected
character): the text now says what the code does, and a replay shows it.
Minors fixed: N1 anchored autocmd-call regexes, N3 a demotion in a
terminal that only its name marks does not take Condition 3, N4 "once
events settle" includes the listener's queued check, N5 the shrink step
names the three two-file rules, N6 the update step names the listener
operators, N7 the `held_after_plugin_edit.lua` comment, N8 statechart
labels for the listener steps, N9 user impact of the listener and
`holdLoose` items, N10 the `--hash-only` time.

- Codex round 4 (`91660323`): security clean. Code lane, two P2 threads,
both fixed in this round: the Rules table delimiter (`2c88f30e`) and the
model that restricted `YouEditByPlugin` to normal mode, so TLC could not
reach a moved changedtick on release (`YouEditByPluginInVisual`,
`YouWriteInVisual`, `FlushIgnoresTick`).
- GPT and Opus verifiers on `91660323`: PASS, with minors. Fixed here:
M1 the Rules table, M4 the `holdLoose` exemption names `HeldInTerminal`,
M5 "the rows whose rule is `none`", M6 the return for an unloaded buffer
in the Claude terminal is in the not-modeled list (I replayed it on
0.8.0 and 0.12.3). M2 and M3 (a regex that misses a blind-spot mutant or
reads through a shared helper) are not changed: the lock reads STALE for
them, as for F4 above.
- Codex round 5 (`f974ee06`): both lanes clean, CI green, no open
threads.
- Opus and GPT verifiers on `f974ee06`: ISSUES, one documentation defect
(F1) and three minors, all fixed in round 6. F1: SKILL.md said that an
edit from a timer, a job or an autocmd cannot hit the same-typeahead
bug. The true boundary is any edit whose check has not run when the next
key arrives. Two more ways to get there are reproduced and have replays
(a key that arrives during the plugin's callback, an autocmd edit at a
mode change), the model, replay and SKILL.md text now say so, and coder#540
fixes all three. M1: `check.sh` prints only the first broken rule, and
`--mutants` shows the others. M2: the operator order sentence
(`on_lines` first, with the mode already normal, then `ModeChanged`) is
fixed. M3: the `ListensToSelectionBuffer` regex and the old fact set
(four facts, shown with `check.sh` itself).
- Codex round 6: this head (the last round).

## Notes for the reviewer

- The diff is one new skill folder: SKILL.md, `check.sh`,
`covered.lock`, `model/` (the TLA+ spec and a `/statechart` view) and
`replays/`. It touches no `lua/` code.
- `DEVELOPMENT.md` is not edited here: the skill-listing change belongs
to the PR that owns it.

---
_Generated with [`xum`](https://github.com/coder/xum) • Model:
`anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant