Repository navigation
fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file - #524
Merged
Conversation
… edits another line or writes the file The flush on leaving visual mode skipped the release whenever the buffer's changedtick had moved since visual mode began. That guard is there for an operator (d, c, >, gU...) that consumes the selection: the '< and '> marks then point at text that was never selected. A plugin's edit of another line, or a :write of a modified buffer, also moves the changedtick, but leaves the selection on the screen. Claude then got the cursor instead of the selection, whether you released it within the debounce (100 ms) or after it. The flush now skips only what an operator did. The listener that already watches the held buffer also watches the buffer you select in. Neovim ends visual mode before an operator changes any text, so an edit that finds visual mode over is an operator's. A plugin's edit leaves visual mode on. A :write fires no callback, so it never counts. 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, so the callback only counts the edit and vim.schedule reads the mode after the call. The flush skips a selection that still has an unchecked edit, which is what an operator leaves, because its flush comes before the check.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Member
Author
|
Integration runner ( |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 65ce284dc9
ℹ️ 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".
…r as they are now The facts file still said that any buffer change in visual mode skips the flush, and that the buffer listener exists only while Claude holds a selection.
…n starts, and re-record covered.lock The Global Side Effects list said that the change listeners are on the buffer of a held selection. They are now also on every buffer where a visual selection starts, until the first edit after it ends. covered.lock: only the hash of selection.lua changed, which cannot reach diff state, an openDiff answer, a disconnect or a diff command. The model passes (89,205 distinct states).
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Nov 12, 2026
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
Resolve the README conflicts with #524 and #530. Main's listener and flush wording for visual selections stays. The root Editor state bullet keeps the verified augroup list and takes main's listener wording. The terminal.setup sentence in lua/claudecode/README.md now names the provider that the warning keeps (#530), which replaces the claim that the warning is wrong.
This was referenced Nov 12, 2026
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
…y in verify-selection-tracking #524 replaced the changedtick comparison in the flush with a visual_entry that the buffer listener marks. Read the new guard (FlushSkipsOperator), the listener that counts a visual edit (ListenerNotesVisualEdit) and the check that spares a plugin's edit (VisualCheckSparesPluginEdit), and keep the old comparison as the fact FlushIgnoresTick (FALSE on the code before #524). The model gets two steps that move only the changedtick while you select: a plugin's edit of another line and a :write.
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
The model reads the new visual_entry guard (FlushSkipsOperator, ListenerNotesVisualEdit, VisualCheckSparesPluginEdit) and the old comparison as FlushIgnoresTick. The hashes of the flush, on_mode_changed and watch_selection_buffer blocks changed, and visual_entry_of and note_visual_edit are new blocks. The file hashes of init.lua and server/init.lua changed with main: no block the model reads changed there.
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
…select, and name the one-typeahead limit Three probes for #524: a plugin edits another line, a plugin appends lines, and :write runs while you are in visual mode, then Esc inside the 100 ms debounce. Claude must get the selection. They print BUG on the code before #524 and OK on main, on Neovim 0.12.3 and 0.8.0. The old limit replay quick_release_after_plugin_edit_in_visual.lua becomes the first one, with the verdict that #524 made true. A mapping that edits and presses Esc in one typeahead still reaches the flush before the check, so that limit gets its own replay.
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
…ree doc minors in verify-selection-tracking Facts table, the #524 path in Bugs this model found, the new step names, the replays table, the holdLoose exemption (HeldInTerminal too), the 'rows whose rule is none' wording, and the unloaded-buffer return in Not modeled.
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
…ad the old listener in ListensToSelectionBuffer Opus and GPT verified f974ee0 and found one documentation defect: 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, and two more ways to get there are reproduced (a key that arrives during the plugin's callback, an autocmd edit at a mode change). They get replays that print BUG until #540 merges. Also: check.sh prints only the first broken rule, the operator order sentence (on_lines first, ModeChanged after) is fixed, and the ListensToSelectionBuffer regex reads both forms of on_lines (it read FALSE on the code before #524, which listens).
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
… it contradicts (coder#533) ## Why The goal is that every claim in the README contracts of this repository is true for the code at `main`, and that each correction names its evidence. A contract is the README of one folder. It states what the code does and cites the function that does it. The branch `docs-gtz7` corrected many claims at an old commit of `main`. `main` has moved since (peer PRs coder#445 to coder#522 rewrote several passages and changed the code). This PR merges `main` into that work, re-checks every line that it changes against the current code, and fixes the lines that the peers made stale or that the merge joined into false text. ## What changed Docs only, in seven README files. The branch has four parts. 1. The commits of `docs-gtz7` (three content commits and a merge of `main`): a refresh of the contracts against the code, a pass that fixed the drift that the refresh left, and a pass that corrected claims which runtime probes disproved. 2. Five merge commits of `main` (the second for coder#522, the third for coder#524 and coder#530, the fourth for coder#506, the fifth for coder#531 and coder#526). Where a peer PR and `docs-gtz7` both changed a passage, `main`'s text won. A `docs-gtz7` correction stayed only where it is still true. 3. Nine correction commits. Six verifier agents, one per file or half file, checked every line that this diff changes against the code. They ran headless Neovim 0.12.3 probes (one on 0.10.4) where reading did not decide the claim. I applied their corrections in commits that group the files: server, root and plugin, tools, lua, terminal, scripts, the main-text fixes, and one for the exit sentences and the last seven findings. A second verifier then found one false sentence (the exit sentence below) and seven wording findings, which that last commit fixes. 4. One commit for two P2 findings of the Codex code review on `42ef1bd1`. First, `stop` and the token mismatch in `start` try to remove the lock file and only log a warning when that fails (`lua/claudecode/init.lua:642-647`, `:605-608`), so three sentences in `README.md` now say "tries to". Second, the headless auto-setup check in `plugin/README.md` used `--cmd "set rtp^=$PWD"`, which Ex splits at a space in the checkout path. I ran it in `/…/with space/repo` on Neovim 0.12.3: it fails with `E518` and prints `0`. The `lua vim.opt.rtp:prepend(vim.fn.getcwd())` form prints `2`, and `0` without the auto-setup line, as the README says. Per file, with the number of claims checked and the result: | File | Claims checked | True | False | Incomplete | Unverified | Edits | |---|---|---|---|---|---|---| | `README.md` (Repository Blueprint) | 41 | 39 | 0 | 2 | 0 | 2 | | `plugin/README.md` | 40 | 39 | 0 | 1 | 0 | 1 | | `lua/claudecode/README.md` | 198 | 173 | 11 | 14 | 0 | 23 | | `lua/claudecode/server/README.md` | 88 | 75 | 3 | 9 | 1 | 13 | | `lua/claudecode/terminal/README.md` | 106 | 100 | 2 | 4 | 0 | 5 | | `lua/claudecode/tools/README.md` | 68 | 54 | 4 | 10 | 0 | 14 | | `scripts/README.md` | 7 | 0 | 2 | 4 | 0 | 13 | A false claim was true at the old base or never true. An incomplete claim leaves out a condition that the code has. The row for `scripts/README.md` lists the seven items of the coder#462 verifiers (one more was misleading). The 541 claims of the first six rows split into 480 true, 20 false, 40 incomplete and 1 unverified. ### Re-sync items after the peer PRs - coder#530 (invalid `provider`). `lua/claudecode/README.md` said that an invalid `provider` keeps the previous value "although the warning says Defaulting to 'native'". `main` now warns `Keeping '<provider>'` (`lua/claudecode/terminal.lua:483-488`). The sentence says what the warning names now. The defect is gone from the list of code defects below. - coder#531 (release-please runner). The `run-release-please.sh` bullet of `scripts/README.md` keeps the verified text and adds `main`'s clause that `commonmark` must be on the module path too. The runner requires it at load (`scripts/release-please-runner.js:27`). The Communique, Prettier and output code that the runner bullet cites did not change. - coder#526 (snacks tests). It changes comments and dead window option assignments in `lua/claudecode/terminal/snacks.lua`. No line of this PR depends on them. - coder#524 (visual selection and plugin edits). The two conflicts were passages about the buffer listener and the flush of a visual selection. `main`'s text won in both, and the root `Editor state` bullet keeps the verified autocmd group list with `main`'s listener wording (`lua/claudecode/selection.lua:watch_selection_buffer`, `note_visual_edit`). The selection claims that this PR changes (`selection_changed` positions, `selection.lua` internals) do not depend on the code that coder#524 changed. - coder#459 (lockfile). `README.md` no longer says that `start` leaves the lock file on disk after a token mismatch: `start` removes it and stops the server (`lua/claudecode/init.lua:603-619`). The System Verification bullet about `CLAUDE_CONFIG_DIR` and `tests/lockfile_test.lua` is gone: the test hides the caller's value and stays in a private home (`tests/lockfile_test.lua:340-355`, `:439-442`). `lockfile.update` is removed from `lua/claudecode/README.md`: the module has no such function. The `start` and `stop` bullets use the text of coder#459, and `stop` is described as an attempt to remove the lock file (`init.lua:635-670`). - coder#461 (openFile reload). The reload-error passage of `lua/claudecode/tools/README.md` is the text of `main`. The claim that the recovery read does not end Visual mode stays. A probe confirmed it in both forms: plain Visual mode, and Visual mode that CTRL-O started. The read runs through `nvim_buf_call`, so the mode stays on (`lua/claudecode/tools/open_file.lua`). - coder#462 (WebSocket shell clients removed). No README cites `scripts/lib_claude.sh` or another deleted file (a grep over the seven files finds none). ### Corrections per file <details> <summary>README.md</summary> - The list of what rejects a pending `openDiff` now includes Claude's `close_tab` and `closeAllDiffTabs` calls, which reject it through `close_diff_by_tab_name` (`lua/claudecode/diff.lua:2040-2044`, `:2105-2107`, `lua/claudecode/tools/close_tab.lua:53`, `lua/claudecode/tools/close_all_diff_tabs.lua:30`). - At exit, Neovim fires `BufUnload` for each loaded buffer before `VimLeavePre`, and the proposal buffer's `BufUnload` autocmd rejects its pending diff (`lua/claudecode/diff.lua:1279-1285`). So with one pending diff the rejection runs before the `VimLeavePre` cleanup. With two or more pending native diffs there is one exception: the reject of a new-file diff in the current tab with `diff_opts.on_new_file_reject = "keep_empty"` (the default) deletes its proposal buffer (`diff.lua:1171-1175`, `:1523-1524`), Neovim's exit loop then stops firing `BufUnload`, and the cleanup removes the other diffs with no answer. Probes on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3 show both cases, and the `unified` layout answers every diff. The sentence states both. A fix PR (F13) follows, see "Defects in the code". - `start` removes the lock file on a token mismatch (see above). - The Processes bullet adds `:checkhealth claudecode` (`<cli> --version`, `lua/claudecode/health.lua:43-66`) and the `git rev-parse` of `terminal.git_repo_cwd` (`lua/claudecode/cwd.lua:28-42`). - `CLAUDE_CONFIG_DIR` set but empty uses `~/.claude/ide` (`lua/claudecode/lockfile.lua:11-18`). Three lines say so now. - The Side Effects bullet lists the autocmd groups of `lua/` and `plugin/` (`ClaudeCodeShutdown`, `ClaudeCodeSelection`, `ClaudeCodeMCPDiff`, `ClaudeCodeDiffCleanup`, `ClaudeCodeNativeAdopted`, `ClaudeCodeOpenFileNewFiles`, and one `snacks_win_<id>` per Snacks terminal whose split the plugin re-creates, `lua/claudecode/terminal/snacks.lua:259`), the `nvim_buf_attach` listeners (`lua/claudecode/selection.lua:175-191`) and the `"unified"` highlight groups (`lua/claudecode/diff_inline.lua:33-36`). </details> <details> <summary>plugin/README.md</summary> - Commands from auto-setup exist after a startup script that waits (`:sleep` or `vim.wait()`) lets the deferred `setup` run. They do not exist when the `-c` commands and `VimEnter` run. Headless probes on Neovim 0.12.3 (`plugin/claudecode.lua:13-17`). - The other 39 changed claims held: the load guard order, the second `source` doing nothing, the version error on Neovim older than 0.8, the failed module load shown once, the auto-setup global read twice, and the error from the deferred `setup`. </details> <details> <summary>lua/claudecode/README.md: 23 corrections with evidence</summary> - Only :ClaudeCodeSend uses the local add_paths_to_claude. :ClaudeCodeTreeAdd and :ClaudeCodeAdd call M.send_at_mention in their own code. Evidence: lua/claudecode/init.lua:703, init.lua:830, init.lua:904, init.lua:914, init.lua:974-975, init.lua:1021-1022, init.lua:1126. - expand_tilde expands only `~` and `~/...`. A path such as `~user/x` stays as it is. Evidence: lua/claudecode/init.lua:1113-1117, lua/claudecode/utils.lua:167-181. - The fallback split runs create_split, whose leave_preview_window moves from the preview window to a tiled Claude terminal window in the same tab before it splits. Evidence: lua/claudecode/diff.lua:803-810, diff.lua:263-276, diff.lua:279-281. - Since coder#483 and coder#469, diff_inline.lua no longer calls _resolve_diff_as_saved (it calls _write_proposal) and it also calls _register_reject_when_hidden and _close_proposal_window. Evidence: lua/claudecode/diff_inline.lua:471, diff_inline.lua:485, diff_inline.lua:616, lua/claudecode/diff.lua:1228-1234, commits 6eef218 (coder#483) and 36f4a0e (coder#469). - lockfile.update no longer exists: PR coder#459 (0e63cc7) removed it. Evidence: lua/claudecode/lockfile.lua:74, lockfile.lua:84, lockfile.lua:208, lockfile.lua:239, lockfile.lua:292 (the only M functions), commit 0e63cc7 (coder#459). - terminal.setup also calls get_provider, whose fallback warnings go through logger.warn, as the bullet above says. Evidence: lua/claudecode/terminal.lua:584, terminal.lua:124-130, terminal.lua:145, terminal.lua:163-166, terminal.lua:178. - A connected send that the debounce queues still fires ClaudeCodeSendComplete. Only the disconnected branch fires none. Evidence: lua/claudecode/init.lua:383-398, lua/claudecode/init.lua:1395-1400, lua/claudecode/init.lua:401-416. - The terminal call and the event happen only when _broadcast_at_mention succeeds. Evidence: lua/claudecode/init.lua:383-400. - No handshake polling exists since coder#454/coder#480. The 50 ms, 25 ms and connection_wait_delay facts repeat main's queue bullet. A send with debouncing off still queues behind a non-empty queue. Evidence: lua/claudecode/init.lua:283-289, lua/claudecode/init.lua:110-111, lua/claudecode/init.lua:1381-1396. - PR coder#452 added TextChangedI and TextChangedP. Evidence: lua/claudecode/selection.lua:387. - Since coder#452 reconcile_held_selection reports the cursor at CursorMoved, not after visual_demotion_delay_ms. A text change and another buffer also end the hold. Evidence: lua/claudecode/selection.lua:237-265, lua/claudecode/selection.lua:118-159, lua/claudecode/selection.lua:576-584, tests/selection_test.lua:2341. - find_main_editor_window skips only a fixed filetype list, not every explorer or outline sidebar. Evidence: lua/claudecode/diff.lua:157-190. - find_main_editor_window can return a window of another tab (current tab first), as the bullet above says. Evidence: lua/claudecode/diff.lua:125-142, lua/claudecode/diff_inline.lua:382-409. - Probe: proposal "a\n\n" is accepted as "a\n" (split_lines drops one trailing empty line, and the newline fix adds none back). Evidence: lua/claudecode/diff_inline.lua:44-52, lua/claudecode/diff_inline.lua:526-540, lua/claudecode/diff_inline.lua:303, probe_unified_accept.out. - An invalid diff percentage falls back to split_width_percentage, not straight to 0.30. Evidence: lua/claudecode/diff.lua:50-69. - PR coder#469 set the unified proposal buffer to bufhidden=hide (main's bullet above says so), WinClosed/BufHidden reject it. Evidence: lua/claudecode/diff_inline.lua:299, lua/claudecode/diff_inline.lua:475-485, lua/claudecode/diff.lua:1189-1222. - The close_tab tool also passes a client_id. Evidence: lua/claudecode/tools/close_tab.lua:53, lua/claudecode/diff.lua:2105-2148. - At qa! the BufUnload autocmd (diff.lua:1283) calls _resolve_diff_as_rejected before the VimLeavePre cleanup runs, for one pending diff. With two or more native diffs, a keep_empty reject of a new-file diff deletes its buffer and stops the exit loop, so the later diffs stay pending until the cleanup (the Augroups bullet states this). Evidence: lua/claudecode/diff.lua:1171-1175, lua/claudecode/diff.lua:1279-1285, lua/claudecode/diff.lua:1523-1524, probes on 0.8.0 to 0.12.3. - PR coder#478 added the WinClosed autocmd that deletes the handler. Evidence: lua/claudecode/diff.lua:455-463, tests/unit/diff_new_tab_terminal_handler_spec.lua:127. - require('claudecode').setup validates log_level (assert) before logger.setup runs. Evidence: lua/claudecode/init.lua:462-465, lua/claudecode/config.lua:15, lua/claudecode/config.lua:98-106, lua/claudecode/logger.lua:26-40. - Neovim 0.10 has no 'messagesopt' and always stops. The parenthetical read as if only 0.11+ stops. Evidence: probe_echospace.out (0.10.4: NO SUCH OPTION, 0.11.5: hit-enter,history:500). - With laststatus=1 and two windows v:echospace is 68, not 51. Evidence: probe_echospace.out. - PR coder#445 removed the skip. The loop runs every file. Evidence: scripts/run_integration_tests_individually.sh:86-88. </details> <details> <summary>lua/claudecode/server/README.md: 13 corrections with evidence</summary> - The pending check/idle pair of a tick runs judge_silence and judge_stall, not only a stall confirmation Evidence: lua/claudecode/server/tcp.lua:601-611, tcp.lua:424-435, tcp.lua:490. - The state stays `closing` after on_close. On_close only removes the client (README line on client states says it never becomes `closed`) Evidence: lua/claudecode/server/client.lua:363-371, tcp.lua:227-228, tcp.lua:275-283. - start_close_timer also sets `closed` when a keepalive window passes with no write progress Evidence: lua/claudecode/server/client.lua:459-466, client.lua:140-144. - Completes the state list: _disconnect_client does not touch client.state (probe: on_disconnect saw state `connected` after EOF) Evidence: lua/claudecode/server/tcp.lua:209-217, tcp.lua:255-294, probe-server/events.log client_8, client_9. - PR coder#480 added connected_at to get_client_info Evidence: lua/claudecode/server/client.lua:522-531, client.lua:292. - PR coder#454 moved process_mention_queue from on_connect to on_open Evidence: lua/claudecode/server/init.lua:57-73, client.lua:294-296. - After the merged sentences, `It` reads as process_data or the Close frame. Process_data does check the whole message Evidence: lua/claudecode/server/frame.lua:156-168, client.lua:184-188. - parse_frame rejects a 1-byte Close payload with 1002 (same bullet group says so), so only an empty payload reaches the 1000 default Evidence: lua/claudecode/server/frame.lua:157-160, client.lua:352-361, probe S5, S6. - Since PR coder#455/coder#488 last_pong plays no part in the keepalive Evidence: lua/claudecode/server/client.lua:381-383, client.lua:529, tcp.lua:220-222, tcp.lua:474-475. - PR coder#497/coder#500: tools/call answers -32602 for a non-string name before handle_invoke. Contradicts the JSON-RPC errors bullet Evidence: lua/claudecode/server/init.lua:353-368. - Two callbacks share the name: process_data's on_error carries client errors (other bullets say so), server.on_error only server failures Evidence: lua/claudecode/server/tcp.lua:121,190,196,524, tcp.lua:229-231, client.lua:202,275. - The 101/error write callback calls on_error when err or not success Evidence: lua/claudecode/server/client.lua:271-279, probe events client_1..3. - The message carries the tool name Evidence: lua/claudecode/tools/init.lua:90-96. </details> <details> <summary>lua/claudecode/terminal/README.md: 5 corrections with evidence</summary> - FALSE since coder#464: native close and the first get_active_bufnr of a module copy adopt a marked live terminal. The sentence also contradicts the same bullet's second sentence. Evidence: lua/claudecode/terminal/native.lua:292, lua/claudecode/terminal/native.lua:574-577, probe probe-terminal/probe_native_reload.out. - INCOMPLETE: on Neovim 0.12.3 termopen also returns 0 under :silent! for a modified buffer, which is not an invalid argument. Evidence: probe probe-terminal/probe_termopen.out (cases D, E, F, G, H, I), lua/claudecode/terminal/native.lua:237-242. - INCOMPLETE: through the dispatcher a missing Snacks never reaches the ERROR notification, because get_provider falls back to native. Evidence: lua/claudecode/terminal.lua:133-146, lua/claudecode/terminal.lua:192-196, lua/claudecode/terminal/snacks.lua:691-693. - INCOMPLETE: an unset snacks_win_opts.position falls back to split_side (left or right), so cc_show re-creates a split itself. Evidence: lua/claudecode/terminal/snacks.lua:374-377. - INCOMPLETE: for an adopted terminal each entry with a config replaces term._cc.config, so it is not the config captured at open. Evidence: lua/claudecode/terminal/snacks.lua:463-474, lua/claudecode/terminal/snacks.lua:646-647, lua/claudecode/terminal/snacks.lua:747. </details> <details> <summary>lua/claudecode/tools/README.md: 14 corrections with evidence</summary> - FALSE after PR coder#500: handle_invoke uses `params.arguments or {}`, so no Lua error and no -32000 (probe p1: openFile/saveDocument -32602, getDiagnostics []). Also contradicted line 17. Evidence: lua/claudecode/tools/init.lua:88, lua/claudecode/server/init.lua:357, probes/p1_static.out. - FALSE: the script loops over every tests/integration/*_spec.lua with no skip. PR coder#445 (a4d3238) made it run command_args_spec again. Evidence: scripts/run_integration_tests_individually.sh:86. - Misleading: bufnr() finds 'file.txt', 'b/file', './dir/../dir/file.txt' and '' (current buffer). Probes p1 and p5. Evidence: lua/claudecode/tools/save_document.lua:31, lua/claudecode/tools/check_document_dirty.lua:27, probes/p1_static.out, probes/p5_bufnr.out. - INCOMPLETE after PR coder#457: with no stored selection it reads the editor (the bullet above says so), so it does not always return the stored selection. Evidence: lua/claudecode/tools/get_current_selection.lua:37-39, :83-95. - INCOMPLETE: the -32603 table is returned, not raised, so build_response sends it as `{ result = ... }`. Also joins the hard-wrapped bullet like the rest of the file. Evidence: lua/claudecode/tools/close_tab.lua:26-33, lua/claudecode/tools/init.lua:180-182, lua/claudecode/server/init.lua:387. - Format: the merge wrapped a quoted error message across two lines inside a code span, so a search for the message misses it. Every other bullet is one line. Evidence: lua/claudecode/tools/open_diff.lua:56. - Coherence: the inserted sentence split 'finds it' from 'Without one', so 'one' no longer names the loaded buffer. The moved claim is TRUE (probe p1). Evidence: lua/claudecode/tools/open_file.lua:133-140, probes/p1_static.out. - INCOMPLETE: expand_tilde leaves `~user/...` unchanged. Evidence: lua/claudecode/utils.lua:167-181, lua/claudecode/tools/open_file.lua:547. - INCOMPLETE: with makeFrontmost=false the answer is the JSON object, and in the middle of a command openFile appends a suffix. Evidence: lua/claudecode/tools/open_file.lua:735, :741, :746-760, probes/p4_openfile_save.out. - INCOMPLETE: source and code are nil (absent from the JSON) when the diagnostic has none. Evidence: lua/claudecode/tools/get_diagnostics.lua:82-83. - INCOMPLETE: nvim_get_current_tabpage() returns a handle. Probe p1: tabpagenr() 2, handle 3, groupIndex/viewColumn 2/3. Evidence: lua/claudecode/tools/get_open_editors.lua:19, :65-66, probes/p1_static.out. - INCOMPLETE: reload_file_buffers skips a modified buffer, and a diff kept for another client does not close. Evidence: lua/claudecode/diff.lua:2015-2018, :2025-2027, :1104. - INCOMPLETE: no API tells which loaded buffers were opened before their file existed. The loop marks every loaded, named, normal buffer whose file is not readable. Evidence: lua/claudecode/tools/open_file.lua:170-179. - INCOMPLETE (minor): with diff_opts.layout = "unified" diff.lua hands the result to diff_inline, which builds it. Evidence: lua/claudecode/diff.lua:1050-1053, lua/claudecode/diff_inline.lua:526-537. </details> <details> <summary>scripts/README.md: 7 items of the coder#462 verifiers, each checked against the scripts</summary> - The CI paragraph named no job for "the same job". It now names the three jobs of `.github/workflows/test.yml` (`unit-tests`, `integration-tests`, `covered-lock`), says that `integration-tests` runs the runner twice (the second time with a `TMPDIR` that holds a space and a `%`), and says that `Required` needs only `unit-tests` and `integration-tests` (`test.yml` lines 52-80, 98-167, 215-234). - `tla/check-lib.sh` exit precedence: 2 wins over 1, and 1 wins over 3. A stale lock plus a broken rule exits 1. `--hash-only` exits 0 or 3, and `--record` exits 0. A script that sources the lib and ends without `tla_main` turns an exit 0 into exit 2. Probed with a fake `curl` and a fake TLC: default with a broken rule and a stale lock gave rc=1, default with a pass and a stale lock rc=3, a broken `TypeOK` rc=2, `--record` on a stale lock rc=0 (`scripts/tla/check-lib.sh:81-84`, `:226-246`, `:313-333`, `:406-419`). - `tla_init` comes right after `SKILL` and `MODEL`, before `covered_block` (`.agents/skills/verify-diff-lifecycle/check.sh:15-29`, `scripts/tla/check-lib.sh:461`). - `run-release-please.sh` prints nothing itself, and exits 1 with no message when `release-please` is missing. The runner's stdout and file outputs are listed: release-please's own log lines go to stdout (info and debug) and stderr (warnings and errors), the `key=value` lines go to `GITHUB_OUTPUT` or to stdout when it is unset, and `--dry-run` prints JSON after the log lines and still runs Communique. Probed without a token and without network: wrapper rc=1 with no output, and `Error: GITHUB_TOKEN must be set` (`scripts/release-please-runner.js:487-492`, `:555`, `:590`, `:614`). - `--record` and `--hash-only` exit before the TLC jar is fetched, so they never download it and need no `java`. A plain run and `--mutants` do. Probe with an empty cache and a fake `curl`: `--hash-only` and `--record` made 0 `curl` calls, a plain run and `--mutants` made 1 and exited 2 (`scripts/tla/check-lib.sh:452-453`, `:147-151`). - The Lua repros: under `nvim -l` an uncaught error prints `E5113` and exits 1, `cquit N` and `os.exit(N)` exit N, and a bare file name run from `scripts/` fails with `module 'claudecode.diff' not found`. In the `:luafile` form of CI an uncaught error falls through to `cquit 2` (probes on Neovim 0.12.3, and `-l` exit 1 on 0.9.5, 0.10.4 and 0.11.5). - `repro_issue_70.sh` and `repro_issue_277.sh` side effects that the file did not list: work dir names, the `att-home` folder, the empty `/tmp/agent-tty/<8 hex>` socket folder and the `homes.json` entry that `agent-tty` leaves, the inherited environment, the three background probes of 70 and their `PORT.lock` files (a SIGKILL leaves the lock), the unpinned diffview.nvim clone of 277, the state and cache files of `NVIM_APPNAME=issue-277`, the `perl` timeouts, and the nested copy under an existing `issue277-artifacts-latest`. A full run of 277 with private dirs took 32 s. A SIGKILL run left the lock file and 3 processes until `agent-tty destroy`. - `manual_test_helper.lua` calls the handler itself, so no response sender is stored for its coroutine. Any resolution after the handler yields (accept, reject, or `qa!`) logs `No global response sender found for coroutine`. It is expected and harmless (all four CI-form runs exited 0). </details> ## Scope - No code changes. `covered.lock` does not change. - Lines of `scripts/README.md` about `repro_issue_218.sh` stay as they are on `main`. PR coder#458 owns them, and its merge will change them. - I checked every line that this diff changes. Lines that the diff does not touch were not re-verified, except where a verifier found one false while reading its neighbors. Those fixes are in the last correction commit: `server/mock.lua` is required by `tests/unit/server/mock_spec.lua`, the augroup and `utils.lua` lists, the empty `CLAUDE_CONFIG_DIR`, and the Processes bullet. - Probes ran on Linux with Neovim 0.12.3. One probe ran on 0.10.4. The old Neovim claims that earlier lanes proved on 0.8 were not run again. - One claim stays unverified: the sentence in `lua/claudecode/server/README.md` that a client whose EOF the server read in the same read as its request is handled as the code says. Six probe tries did not produce that case. The sentence is a softening, so I kept it. - The terminal README says that the wait before a `close` does not prevent a hang at exit. A probe saw the hang with and without a `close`, so the probe does not prove that the buffer delete causes it. I did not open neovim/neovim#42508 (the host has no network). ### Defects in the code that the verifiers found These need a code fix and a test, so they are not in this docs PR. 1. Accepting a `unified` diff drops one trailing empty line of the proposal: `"a\n\n"` is accepted as `"a\n"` (`lua/claudecode/diff_inline.lua:44-52` and `:531`). The native layout is not affected. A probe shows it. The README says the accepted text is the proposal lines that setup computed. 2. `lua/claudecode/server/tcp.lua:19` says the PRNG is seeded once per process. It is seeded once per load of the module. 3. `lua/claudecode/server/init.lua:59-60` logs "Authenticated WebSocket client connected" from `on_connect`, before the authentication check runs. 4. `lua/claudecode/cwd.lua:36-42` runs the same `git rev-parse` twice. 5. At exit, a pending native diff can stay unanswered. Two native diffs are pending, and the first one (the lower proposal buffer number) is a new file in the current tab with `diff_opts.on_new_file_reject = "keep_empty"` (the default). On `:qa!` its reject deletes its proposal buffer (`lua/claudecode/diff.lua:1171-1175`, `:1523-1524`), Neovim's exit loop stops firing `BufUnload` (`src/nvim/main.c`, the `bufref_valid` check), and the `VimLeavePre` cleanup removes the second diff with no answer. Reproduced on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3, with and without the server. A separate PR (F13) will make exit answer every pending diff. It will change the exit sentences of this PR: the openDiff bullet in `README.md` (Global Invariants, the sentence that starts "When Neovim exits") and the Augroups bullet in `lua/claudecode/README.md` (the sentences about `BufUnload` and the exception). ## Blast Radius Seven README files. Nothing loads them at runtime. A wrong correction here misleads a reader but breaks no behavior. ## Verification - Six Opus verifiers, one per file (two for the 198 claims of `lua/claudecode/README.md`). Each checked every claim that the diff adds or changes against the code, and every `[file:symbol]` citation, with file and line evidence. Their findings, edits and probe scripts are in the evidence folder of the run. - A second, independent verifier checked the head `bcacd14c` (134 sentences and all seven scripts items, with probes on Neovim 0.8.0 to 0.12.3). It found one false sentence (the exit sentence, now fixed with its exception) and seven wording findings (fixed). It found no other false claim. - Citation check on the final head: 760 citations, links and test paths over the seven files, 1 flagged. The flagged one is `[plugin/claudecode.lua:pcall(require, "claudecode")]`, an expression that `main` already cites in that README. - `mise run all`: exit 0 on the final head `e3e48af1` (1682 successes, 0 failures, 0 errors, 24 pending, `luacheck` 0 warnings and 0 errors in 178 files). `mise run format-check`: exit 0 on the final head (355 files, 0 changed). 1676 successes, 0 failures, 0 errors, 24 pending. `luacheck` reports 0 warnings and 0 errors in 178 files. The format step changes 0 files. - `git merge-tree --write-tree` of the head and `origin/main` (`3a0bb769`) is clean. - The merges of coder#524 and coder#530 changed one sentence of `lua/claudecode/README.md` and merged two conflict hunks. I checked that sentence and the merged bullets against `lua/claudecode/terminal.lua` and `lua/claudecode/selection.lua` at `a41254a4`. I did not run a verifier agent over the merge delta. --- _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`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…oder#540) ## What a user sees You select text in visual mode, a plugin or a mapping edits another line, and your Esc is read before the plugin has checked that edit. The selection is untouched and its text is still there, but Claude gets the cursor and not the selection. coder#524 fixed the case in which the check ran before the key. Three ways to read the key first also failed on `main`, and this PR fixes all of them: 1. A mapping that edits and presses Esc in one key sequence, for example `<Cmd>lua edit_other_line()<CR><Esc>`. 2. A key that arrives while a callback runs, as a UI sends it (`nvim_input`): during the plugin's own timer callback, or during another one that was queued before the check. 3. An autocmd that edits when visual mode starts (a `ModeChanged` handler for `n:v`) with the Esc already in the typeahead (`ve<Esc>`). The replays of `verify-selection-tracking` print `BUG` on `main` for each of them, 3 of 3 runs on Neovim 0.8.0 and 0.12.3, and `OK` with this change. ## Cause The flush on visual exit skips a selection that has an edit nobody checked yet (`entry.consumed or entry.unchecked_edits > 0`). An operator (`d`, `c`, `>`) edits the text and then ends visual mode, and its flush runs before any check, so that skip is what stops a phantom selection. A plugin's edit leaves visual mode on. The check that tells the two apart (is visual mode still on?) ran only in `vim.schedule`, and a schedule runs after the command or callback that made the edit returns, and after any callback that was queued before it. When a key is read first, the flush takes the plugin's edit for an operator's. ## The fix `lua/claudecode/selection.lua`: - `check_visual_edits(entry)` is the old scheduled check as its own function. It judges every edit that is waiting at once, by the mode that they left (visual mode on: a plugin's edit, benign. Off: an operator consumed the selection). It does nothing for a stale entry or when nothing waits, so running it twice is safe. - `note_visual_edit` still counts the edit and schedules the check, and it now also sets a `vim.on_key` listener (one namespace, made on first use). Neovim calls the listener for the next key before it processes that key, also for a key that comes from a mapping or that a UI sends, so the Esc finds visual mode still on. Whichever of the schedule and the key comes first runs the check, and the check clears the listener. - An operator's flush still comes before both, so `d`, `c`, `>` and the other operators skip as before. A listener of a flushed selection does nothing at the next key and clears itself, so it can live until that key (README says "at the latest until the next key"). I checked the key listener on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3 (a probe script, not the plugin): it fires for the `<Esc>` of a mapping before it is processed with the mode still `v`, a second `vim.on_key(fn, ns)` replaces the first, and `vim.on_key(nil, ns)` is safe inside the callback and for an unregistered namespace. I did not try the range of the edit (`on_lines` receives the changed lines) as the test for whether it touched the selected lines. By my reasoning, which I did not test, a plugin edit inside the selection would then count as an operator's although the selection is still on the screen, and the marks and the edit range can be in different coordinates once lines move. ## Proof - `tests/integration/selection_visual_edit_spec.lua` has eight new real-Neovim cases: a mapping edits another line and presses Esc, appends lines and presses Esc, edits twice and presses Esc, writes the file and presses Esc, edits and then `d` (nothing is sent after it), an operator followed by the next selection in one typeahead, an autocmd edit at a mode change with `ve<Esc>`, and a queued check that runs after visual mode ended and before the flush (a user `ModeChanged` handler for `*:n` that calls `vim.wait(0)`, defined before the plugin starts, and a mapping that edits and presses Esc). On `main`'s `selection.lua` five of them fail on Neovim 0.8.0 and 0.12.3 (the first three, the autocmd case and the new one), and the rest are guards. The spec passes 20 of 20 on 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3. The case for a key that arrives during a callback is a replay only: `vim.wait` gives the callback's key a main-loop turn first, so the check cannot lose the race in that spec. - `tests/selection_test.lua` has eleven new cases (the mock gets `vim.on_key` and one `nvim_create_namespace` id for each name, a new one for the empty name, as Neovim does): the key comes before the schedule, a check that runs after visual mode ended and before the flush judges nothing again, several edits are judged together, the edit of a mapping is not the operator that comes next, a stale check does not clear the listener of the next selection, the schedule clears the listener, several edits keep one listener, a stale listener clears itself, an operator's listener waits for a key, and (the last two) a detached listener counts as an operator on the visual entry and the detach of another buffer does not. I changed `selection.lua` in 14 ways, one at a time, and counted the failures in `tests/selection_test.lua` (158 cases): no key listener (9), a listener that only clears (4), one decrement for each check (1), never consumed (6), always consumed (6), no schedule (6), no `clear_visual_edit_keys()` in the key listener (2), no `clear_visual_edit_keys()` in `check_visual_edits` (1), a `clear_visual_edit_keys` that does nothing, which removes both (4), a namespace for each edit (3), no stale-entry guard (1), no `unchecked_edits == 0` guard (1), and no `entry.consumed = true` in `on_detach` (1). 13 are killed. One survives and I think it is equivalent, but I did not prove it: the key listener checks `M.state.visual_entry` instead of the entry it was set for. The listener always belongs to the last noted entry, and a different current entry has no unchecked edit, so the zero guard returns. The zero guard itself is not equivalent. A `ModeChanged` handler that runs before the plugin's and calls `vim.wait(0)` runs the queued check after visual mode ended and before the flush. Without the guard that check judges the edit a second time, takes it for an operator's, and Claude gets the cursor. The new unit case and the new integration case kill it (the integration case on Neovim 0.8.0 and 0.12.3). - `verify-selection-tracking` (merged in coder#477): `check.sh` passes (129,986 distinct states) and so does `verify-diff-lifecycle` (89,205), with both locks re-recorded: `selection.lua` changed, the selection skill has a new covered block (`check_visual_edits`), and the diff model reads no block or site of that file. All 16 replays print `OK` on Neovim 0.8.0 and 0.12.3 at the default delay and with `DELAY_MS=50`. The three that replay these bugs print `BUG` on `main`. - The skill is updated for this fix: `VisualCheckSparesPluginEdit` now reads `check_visual_edits` and both triggers in `note_visual_edit`, so removing the schedule, the key listener, the mode test or the `consumed` mark reads `FALSE` and nothing else (checked with five mutants of `selection.lua`; the model then breaks `ReleaseSent`). `ListensToSelectionBuffer` reads `check_soon()` in the body of `on_lines` (in the branch that holds the selection) and in the body of `on_reload`, each body on its own. So moving the call into the `elseif not entry` branch, removing it from `on_lines` or `on_reload`, or moving it from `on_reload` into `on_detach` reads `FALSE` and nothing else (five mutants). All 27 facts read `TRUE` on this tree. On the code before coder#524 exactly four facts read `FALSE` (checked at the previous push), and the old form of `on_lines` still reads `TRUE` for `ListensToSelectionBuffer` after this change. The replay header prints the Neovim version as numbers (it printed a table address on 0.8). - Gates on the final head: the full unit suite (`busted --shuffle`, seed 1794484841) 1748 successes, 0 failures, 28 pending. The integration runner (CI style, a private `HOME`, normal and `odd tmp 50%` `TMPDIR`): 535 tests in both runs on 0.12.3 and 398 in both runs on v0.8.0, 0 failures, and the real cache stays untouched. `scripts/tla/test-check-lib.sh` 44 of 44. The spec passes 20 of 20 on all five Neovim versions, `selection_test.lua` 158 of 158, `check.sh` of both skills passes, `luacheck` 0 warnings in 185 files, `treefmt --ci` 0 changes in 427 files, and `--hash-only` matches for all four `verify-*` skills (no re-record was needed after the merge of `main`). - `selection_held_spec.lua` is flaky under load on `main` (here 7 of 72 runs, on `origin/main` 14 of 72). This PR does not touch it. coder#559 fixes it with condition waits and shows the cause with traces. ## Notes for the reviewer - coder#553 is merged. This branch merges `main` and keeps the helpers of that PR at the outer scope of the spec, because the mapping cases use them. coder#559 also edits `selection_visual_edit_spec.lua` (`wait_for_cursor` waits 400 ms, and one new case at the end of the operator block), so whichever of the two lands second needs a small merge in that file. - Neovim 0.8 and 0.9 still need the scheduled check for a plugin edit whose callback ends before any key (their `on_lines` runs with visual mode off during the API call). The key listener adds the keys that come first. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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, thenEscwithin 100 ms. Claude got the cursor (a.txt "" 0:4-0:4). After: Claude holdsalpha.Cause
flush_visual_selectionskips the release onEscwhen the buffer's changedtick moved since visual mode began (the guard from #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:writeof 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
:writefires no buffer callback at all.watch_selection_buffer(the fix(selection): end a held selection when its file changes while you are in the Claude terminal #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.visual_entryno longer stores a changedtick. It storesconsumedandunchecked_edits. The flush skips whenconsumedis set or an edit is unchecked.nvim_buf_set_linesornvim_buf_set_textcall, and run the callback in that state (0.10 and later run it in visual mode). So the callback only counts the edit, andvim.schedulereads 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
d,c,>, a linewise>, and an operator after a plugin's edit or after a:write.gU,~,J) stay skipped, as the old comment says.Escare 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.Tests
tests/integration/selection_visual_edit_spec.lua(new, real Neovim):writeof a modified buffer. Guards:ved,vec,Vj>,dafter a plugin edit,dafter a:write. Next selection does not inherit an operator.tests/selection_test.lua: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
:writecases 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 --ciis 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 aTMPDIRnamedodd tmp 50%, in a privateHOME, passes 331 tests per run on 0.12.3 and 244 per run on 0.8.0, with 0 failures.verify-diff-lifecycle/check.shmatches after the re-record: only the hash ofselection.luachanged, which cannot reach diff state, and the model passes (89,205 distinct states). The docs say what the listeners do (lua/claudecode/README.mdand the Global Side Effects list inREADME.md).Follow-up
verify-selection-tracking(#477) models the changedtick. It gets a separate round after this merges.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh