Repository navigation
fix(diff): keep the sign column and diff mode the user sets in windows a closed diff leaves - #491
Conversation
…al window The unified layout set 'signcolumn' to yes with the window's default value as well, so a window the user switched to another buffer kept showing yes, and the cleanup gave it the old value back even when the user had set one of their own after the switch. The layout now sets it for the proposal buffer only (local scope): a kept window shows the sign column it had before the diff, and a value the user sets there stays. The cleanup has nothing to restore any more. The journey script gets a step for the user's own sign column, and the skill doc names every command the journey runs. Refs #483 _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
|
@codex review |
|
@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. |
|
Codex Review: Didn't find any major issues. Keep it up! 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". |
🛡️ 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. |
…r original window The split layout's cleanup ran :diffoff in every window it kept, so a diff mode that the user turned on after an :edit ended at close_tab. It now ends diff mode only in a kept window that still shows the file's own buffer, the one case where :edit leaves the diff's diff mode on. A window that shows another buffer has left diff mode, so its diff mode is the user's. The proposal window's :diffoff moves into the split-only branch of the cleanup, so the unified layout cannot reach it. Specs cover the user's diff mode in the proposal window (both layouts), in an original-side window the user switched (two windows in diff mode, because Neovim's 'closeoff' ends a lone one when the proposal window closes), and in a unified window that :edit # switched back to the file. The journey script's header names the step for the user's own sign column and drops a stale comment, and the README cites setup_inline_diff. Refs #483 _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
|
@codex review |
|
@codex security review |
|
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". |
🛡️ 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. |
…window The README said a diff mode that the user turns on in a kept window stays. Neovim's default 'closeoff' turns diff mode off in the last window that has it when another diff window closes. That reaches 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. A user's diff mode over two or more windows stays. Refs #483 _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. Swish! 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". |
🛡️ 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. |
The merge brings in #491, which sets the unified proposal window's sign column with local scope and runs :diffoff in a kept window only while it shows the file's own buffer. covered.lock is re-recorded on the merged code. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
…p one waiting autocmd per file The message of 05d6471 said that `diffoff` does nothing in a window that is not in diff mode. That is wrong: `diffoff` sets 'foldmethod' and 'scrollbind' back to their values from before the diff even when 'diff' is already off. The check on 'diff' is back, so options that the user set after turning diff mode off stay. - The autocmd runs `diffoff` only in the window the event fired for. A waiting window that got the file without a BufWinEnter event (`:noautocmd buffer`, a non-nested autocmd) is dropped without `diffoff`, because the user can have turned diff mode on there since, and a later `:tabnew <file>` no longer ends it. - One BufWinEnter autocmd serves a file's buffer however many diffs leave windows behind. Closed windows and wiped buffers are forgotten when the next diff arms. - README: one statement for what `:edit` does to diff mode, and what the cleanup resets. - Specs: the cases that failed on 05d6471 (own `:diffoff`, both orders of the entry without an event, one autocmd per file, the registry after a wipe) and the cases that keep the autocmd from running `diffoff!`, from ending a diff in another tab, and from acting in a window that is not the entered one. Refs #491, #483. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
…ew windows a saved set without diff mode Round 2 said that a waiting window that got the file without a BufWinEnter event is dropped without `diffoff`. That holds only when the file next enters another window with an event. If the user starts a diff in that window and then leaves the file or reloads it there, the waiting autocmd still ended the user's diff. - The waiting autocmd listens to BufLeave and BufUnload of the file as well as BufWinEnter. Any of them shows that a waiting window already has the file, so the window stops waiting and its diff mode is the user's. `:edit` and `:edit!` raise BufUnload, leaving the window raises BufLeave. The autocmd deletes itself by id, because returning true from a callback deletes only the event that fired. - A window that never showed the file takes the newest set of options saved for it. After a diff window left the file, that set has diff mode on, so `:split <file>` opened a window in diff mode and the next openDiff opened in a new tab. The cleanup now shows the file once in a hidden float with 'eventignore' set to all, runs `diffoff` there while 'diff' is on, and closes the float, so the newest set has diff mode off. No window of the user changes. It skips a file buffer that is unloaded or has 'bufhidden' set. The waiting autocmd stays: a window that left the file takes its own saved set first, and the float does not change that set. - The registry of waiting windows and its test accessor are gone. Each autocmd now prunes closed windows at the next event of the file and deletes itself when no window is left, and every later diff of the file raises such events. - The comment in the cleanup that said `:edit` clears 'diff' only when the new buffer is in no other diff window is gone, and the README states the rule that Neovim follows. Refs #491, #483. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
…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`_
…diff closes (coder#494) ## Why After a split diff closes, a window that still shows the file can stay in diff mode with no partner window. The next `openDiff` then sees a window in diff mode, opens in a new tab, and closes the user's window together with that tab. coder#491 ended diff mode in the windows that the cleanup knew about. This closes the windows that it did not. Refs coder#491, coder#483. ## Cause Neovim saves a window's options for a buffer when the buffer leaves the window ('diff', 'scrollbind', 'foldmethod' and the rest included), and sets them again when that buffer enters the window. A window that never showed the buffer can also take diff mode on, by copying the options of a window that shows the buffer (`:split <file>` copies the window that it splits). While a split diff is open, the file's buffer is in diff mode in the original-side window. So when the cleanup closes the proposal window and deletes the proposal buffer, a window can end up showing the file in diff mode with no partner. Two ways, both reproduced on current main with real Neovim 0.12.3 and v0.8.0: 1. `:b <proposal>` in the original window, then `close_tab`. The cleanup deletes the proposal buffer, the window falls back to the file, and the saved options turn diff mode on. One window, `diff=true`. 2. `:split <file>` from the original window during the diff, then `close_tab`. The copy took diff mode from its source, the cleanup closes the proposal window, and the copy keeps diff mode alone. It stays on when `close_tab` runs from a plain window of the same tab, or from another tab. ## What changed The rule: when the cleanup is done, a window of the original side's tab page that shows the file leaves diff mode only if it is the only window with diff mode on in that tab page. A diff needs a partner window, so a lone diff window holds the leftover of the diff that ended, and a diff of the user's own over two or more windows stays. - `lua/claudecode/diff.lua`: two local functions and one call. `end_diff_mode_if_alone(win)` runs `diffoff` in a window while `'diff'` is on there and no other window of its tab page has `'diff'` on. It catches the refusal that Neovim gives in the command-line window (E11). `end_diff_mode_in_windows_that_show_the_file(diff_data)` runs that check for each window of the original side's tab page that shows the file. The cleanup calls it after the buffer deletes and before `ClaudeCodeDiffClosed` fires, so nothing that a handler of that event starts is looked at. Nothing is recorded and no autocmd is added. - `lua/claudecode/README.md`: states the rule, and which cases stay as on main (below). The sentences on saved options and on the unified layout's `'signcolumn'` are rewritten from plain-Neovim probes. - `tests/integration/diff_left_window_spec.lua` (real Neovim): 33 cases. They cover the two ways above, a window that the diff never left, a copy that has a partner and two copies that the user compares (kept), the options that the user set after ending diff mode, a lone diff window of another tab (not touched), the order of the look and the event (a diff that a `ClaudeCodeDiffClosed` handler starts stays), `close_tab` from the command-line window (it answers TAB_CLOSED and the copy keeps its diff mode, because Neovim refuses `diffoff` there), and the cases below that stay as on main. - Verify skill: `journey-diff-close-save.sh` shows the proposal in the original window with `:b` and closes the diff for an existing file, and `features/open-diff.md` and `SKILL.md` describe it. - `covered.lock` is re-recorded after merging main. Against main's lock only the `diff.lua` file hash and the `cleanup_state` block hash change. `check.sh` passes with TLC (89205 states). ## What stays as on main A file that comes back to a window later gets the options that Neovim saved or copies, diff mode included, as on main: - `:e other.txt` in the proposal window, `close_tab`, then `:e <file>` there, or `:e third.txt` in the original window, `close_tab`, then `:e #`. Diff mode is on again. This is the common case. It gets its own follow-up PR that fixes it at the source: the plugin splits the window before it runs `diffthis`, in both open paths, so the saved set never holds diff mode. - `:split <file>` from a window that left the file after the diff. - A window of another tab page that took diff mode from the diff's windows during the diff (`:tabnew <file>`, `:tab sbuffer`, `:tabnew` then `:buffer <file>`). The look covers only the tab page of the original side. - A `ClaudeCodeDiffClosed` handler that brings the file back into a window. - `close_tab` from the command-line window (`q:`) when the original-side window shows the file fails with -32000 and E11 in main's own `diffoff`, as on main. ## Before and after Real headless Neovim, the plugin's own `openDiff` and `close_tab` tool handlers, a stub `claude` first on PATH: | Scenario | main | this branch | | --- | --- | --- | | 1. original window: `:b <proposal>`, `close_tab` | one window, `diff=true` | one window, `diff=false` | | 2. `:split <file>` from the original window during the diff, `close_tab` from a plain window of the same tab | copy `diff=true`, the plain window's `'foldmethod'`, `'scrollbind'` and `'wrap'` kept | copy `diff=false`, the plain window's options kept | | 3. same copy, `close_tab` from another tab that holds the user's `diffthis` over two windows | copy `diff=true` | copy `diff=false`, the other tab's diff kept | | 4. a window of the first diff that the user switched to another file, then a second `openDiff`, `:edit <file>` in that window, and the second `close_tab` | one window left in diff mode | no window in diff mode | | 5. a copy that has a partner, or two copies that the user compares | kept | kept | | 6. `:e other.txt` in the proposal window, `close_tab`, `:e <file>` | `diff=true` | `diff=true` (follow-up PR) | | a diff with no window switch | `diff=false` | `diff=false` | The same rows give the same result on 0.12.3 and v0.8.0. ## Validation Head 06bde3e (round 9: a merge-only push of main 884f7e2 that re-records `covered.lock`, with no Lua change and no Codex review; the Lua patch-id equals rounds 7 and 8). On it: `check.sh --hash-only` and `check.sh` pass, the coder#494 spec passes 33/33 on Neovim 0.12.3 and v0.8.0, `mise run all` passes (1737 successes), the integration runner passes (527 on 0.12.3 after one rerun of two load timeouts, 390 on v0.8.0), and CI is green. Head e80a5a3, a merge of main 8b77e7e into c219b15 (round 8: a merge-only push, no code change). The PR's Lua diff is the same before and after the merge: `git diff c9e57d1..c219b15 -- '*.lua'` and `git diff origin/main...HEAD -- '*.lua'` give the same patch-id (`76da21f7b53bfdadb02303aa6ef201c9f445de4e`) and the same text without the `index` lines and hunk numbers (main moved `diff.lua`, so those differ). The merge conflicted in `covered.lock` and in `lua/claudecode/README.md`. The README conflict was main's edits around the cleanup bullet (coder#549, coder#542 and others) against the one bullet that this PR rewrites: I kept every line of main and put this PR's bullet in place of the old one, so the README differs from main by that one line. I re-recorded `covered.lock` with `check.sh --record` on the merge result. Against main's lock only the `diff.lua` file hash and the `cleanup_state` block hash differ. Size against main: 7 files, 613 insertions(+), 7 deletions(-). Code and README: 2 files, 42 insertions(+), 3 deletions(-). The spec is most of the rest. - `mise run clean && mise run all` on the merge result: exit 0. luacheck 0 warnings, 0 errors in 182 files. busted 1706 successes, 0 failures, 0 errors, 26 pending. - New spec, 33 cases, on 0.12.3 and on v0.8.0: 0 fail on this branch and 3 fail on main (cases 1 and 2 above, and the one for `close_tab` from another tab). It also passes 33 of 33 on both versions on the merge of this head with the newest main (e4c56fd), which merges without a conflict, and `check.sh --hash-only` passes on that merge. - Integration runner with a stub `claude` first on PATH: 0.12.3 450 successes and v0.8.0 342, 0 failed, 0 errors (28 files). Under `TMPDIR="<dir>/odd tmp 50%"` the same: 450 and 342, 0 failed, and the cache folder stays untouched. - Journey `journey-diff-close-save.sh` in agent-tty with the scripted client (run on c219b15, before the merge): 4 of 4 runs pass (split and unified, existing and new file). Existing file: 24 checks. New file: 23. - Live probes through the plugin's own tool handlers (run on c219b15 against main c9e57d1, before the merge, which changes none of the PR's Lua), on 0.12.3 and v0.8.0, compared by scenario and check name (checks that fail on the head and pass on main: 0 in every set): | Probe set | checks | fail on head | fail on main | fail on head only | fixed on head | | --- | --- | --- | --- | --- | --- | | round-3 verifier | 432 | 97 | 101 | 0 | 4 | | gpt round-3 | 92 | 14 | 14 | 0 | 0 | | round-4 verifier | 106 | 21 | 29 | 0 | 8 | | round-5 verifier | 116 | 56 | 56 | 0 | 0 | | gpt round-5 novel | 46 | 8 | 8 | 0 | 0 | | other-tab | 18 | 12 | 12 | 0 | 0 | | Opus round-6 (copies, handlers, command-line window) | 84 | 20 | 24 | 0 | 2 | | gpt round-6 | 60 | 12 | 12 | 0 | 0 | The 8 fixed checks of the round-4 set are the `:split` copy cases (row 2 and 3), the 4 of the round-3 set are `:b <proposal>` (row 1) and the second diff (row 4), the 2 of the Opus set are the second diff. - Order matrices (handlers that switch focus, raise or open windows, before or after, for `BufEnter`, `BufWinEnter`, `WinNew`, `WinEnter`): gpt's 96 orders per version, Opus's 96 orders (48 per version) and my 40 orders (20 per version) give the same answer, in every field, on this head and on main. A focus probe with a user `BufWinEnter` and `BufEnter` handler that moves the focus to another tab gives the same answer on both. - Probes of the defects that review found in the earlier design (a `:split` copy with a lone user `:diffthis` that gets the file back with `:edit!`, `:e other` and `:e #`, and a window that got the file without a `BufWinEnter`): this head keeps the user's diff in all, as main does. - Mutation: 14 mutants of the new code (no call, no `diffoff`, no `'diff'` check, no partner check, partner in any tab, look in any tab, skip the original-side window, no catch of the refusal, no `nvim_win_call`, the partner must show another buffer, the call after the event, the call before the deletes, no buffer and window guard, `diffoff!`). 13 are caught by the spec on both versions: 12 as failed cases and the one without the guard as an "Invalid window id" error. The survivor is `diffoff!` for `diffoff`. It is equivalent: the check runs first, so no other window in the tab has `'diff'` on, and `diffoff!` acts only on windows with `'diff'` on. - `check.sh --hash-only`: covered.lock matches the code. `check.sh` (TLC, 89205 states, and 5269 for the live model): pass. ## Round limit The maintainer waived the review-round limit for one push (round 7): coder#494 (comment). A second waiver covers one merge-only push (round 8, this head): coder#494 (comment). The push replaces the earlier `BufWinEnter` waiter and its window records with the single look above and merges current main. There is no further push to this PR. A new security flaw, data loss or broken core behavior compared with main ends it as blocked. A third waiver covers one bounded merge-only push (round 9) with no Codex review, and declines the round-8 Codex P1 with a reason: coder#494 (comment). --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
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 calledclose_tab. Two things were overwritten::setlocal signcolumn=yes:2becameauto).:diffoffin every window it kept, so a:diffthisor:setlocal diffthat the user ran after the:editended atclose_tab. Main has this too.What changed
diff_inline.luasets'signcolumn'toyeswithscope = "local", like:setlocal.nvim_set_option_value(..., { win = ... })behaves like:setand also sets the window's default, which every buffer shown there later inherits. fix(diff): leave no leftovers after :wq, a second :w, :qa or :edit #483 hid that by restoring the old value unconditionally, and that restore overwrote the user's choice. With local scope the window showsyesfor 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:diffoffin a kept window only while that window still shows the file's own buffer.:editto 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:diffoffmoves into the split-only branch of_cleanup_diff_state, so the unified layout cannot reach it.SKILL.mdnames every command the journey runs, including:b hello.txt, except the:onlyresets between steps. The README claim about the cleanup is updated and citessetup_inline_diff.covered.lockis re-recorded. The changed code is one window-option call insetup_inline_diffand the window-handling lines of_cleanup_diff_stateand_close_proposal_window. None of it touches how a diff is resolved, closed or answered, andcheck.shpasses.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
:editor:balready gave the window its own value back, the guard skipped the restore and left the window default atyes, so the next:edit third.txtin 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::editanother file, set the option, thenclose_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:diffoffonly when the buffer was put in diff mode in that window, and:editclears that state.'diff'itself is different::diffoffalways 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 containscloseoff), 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. Withcloseoffremoved fromdiffopt, a lone window stays too, in both cases (checked on Neovim 0.12.3 and v0.8.0).Evidence
Before this PR, on the #483 merge commit:
nowhere the user setyes:2).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.luafails 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:
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).mise run all: exit 0, 1341 successes, 0 failures, 16 pending (after the merge of fix(selection): end a held selection when its file changes while you are in the Claude terminal #481). The integration runner passes 254 cases on 0.12.3 and 171 on v0.8.0, with the stubclaudefirst on PATH. The runner's own "Total Success" line adds one summary line per file, so it reads 272 and 189.Mutants, each turns the named spec case red:
scope = "local": 10 cases (both "keeps the 'signcolumn'..." groups).:diffoff: "turns off diff mode in a proposal window that :edit # switched back to the file".:diffoff: "does not close the reused target window when the old file is already open" (unit spec).:diffoffof 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 #483
Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh