From f3103a6953d42b27aceb94b1d6bc631d8f725ba6 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 16:47:54 -0400 Subject: [PATCH] fix(lean4): defer the expansion past the chain, and guard its point MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three defects, all about what happens AROUND the expansion rather than about resolving an abbreviation. A pair character that TERMINATES an abbreviation never reached auto-pairing: `\alp(` gave `α(`. Q#LN22 already said the terminator is not claimed and the implementation claimed it whenever an expansion succeeded. Merely declining is not enough either — the chain hands each consumer a copy of the record made before any consumer ran, so expanding inside the chain invalidates the copy pairing is holding and the closer is silently lost. Verified by mutation rather than assumed: expand-then-decline reproduces `α(` exactly. The expansion therefore runs on its OWN `buffer.after-edit` subscriber, registered after typed_edit.lua's and before lsp.lua's. A claim stops the chain but not a separate subscriber, which is the point: pairing claims the terminator it reacts to. The replaced span now covers only the leader and the typed text, so pairing's closer lands outside it and survives. One undo restores the same text either way, because the terminator was always its own insert. That second subscriber is a new instance of Q#AP7 — lsp.lua flushes didChange synchronously on the signature-trigger path, and `(` is a trigger — so acceptance 45m pins it with the sighelp fake server: no didChange may ever carry the unexpanded text. The relevance check is now three-part, as pairing's has been since #110: buffer, window, AND `ed.cursor() == rec.post_cursor`. A redefined self-insert can insert the completing character and then move the point, and expanding over a span the user has left teleports them back into it. Cursor placement after the replace is context-guarded, as `repair_cursor` is. A buffer intercept may switch buffers while `buf:replace` runs; the unguarded `goto_byte` then translated the Lean buffer's pre-edit point through the Lean buffer's edit and applied it to whatever was ambient. Q#LN22, criterion 38's span wording, and the ledger are corrected to describe the deferred design rather than the one that shipped — the rationale's source, not only the sites quoting it. Acceptance 45j/45k/ 45l/45m added; framing rev 10. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/lean_input.lua | 192 ++++++++++++++++++++------ docs/active-work.md | 25 +++- docs/agent-handoff.md | 9 +- docs/lean4-mode-framing.md | 112 +++++++++++++-- tests/lean_input_acceptance.rs | 241 +++++++++++++++++++++++++++++++++ 5 files changed, 523 insertions(+), 56 deletions(-) diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua index da24378..7b205d2 100644 --- a/builtin/runtime/lean_input.lua +++ b/builtin/runtime/lean_input.lua @@ -124,6 +124,10 @@ end -- TUI-plus-GPU configuration this project ships. local pending = {} +-- Expansions the chain consumer decided on but did NOT perform, keyed +-- the same way. See `run_deferred` below for why they wait. +local deferred = {} + local function frontend_id() local ok, id = pcall(function() return pmacs.frontend.id() end) if ok then return id end @@ -157,19 +161,38 @@ end -- Expansion -- --------------------------------------------------------------------- --- Replace the pending span with `symbol`, placing the point at --- `$CURSOR` if the symbol carries one. Returns the byte offset just --- past the replacement, or nil when the edit was rejected or altered. +-- Right-gravity translation of `pos` through the effective edit — +-- pair.lua's shape, for the same reason: the point sits AFTER the +-- replaced span (on the terminator, or on a closer pairing inserted) +-- and has to move with it. +local function translate(pos, estart, estop, einserted) + if pos < estart then return pos end + if pos > estop then return pos - (estop - estart) + einserted end + return estart + einserted +end + +-- Replace the pending span (leader + typed text) with `symbol`. -- --- ONE `buf:replace` for the whole expansion: one undo step, one CRDT --- op, one effective-edit verification. A rejection drops the pending --- state and does not retry, the same discipline as comment.lua's Q#CT5 --- and pair.lua. -local function expand(buf, p, symbol, span_end) +-- The span deliberately STOPS BEFORE the terminator. Including the +-- terminator would make the expansion and the terminator one edit, but +-- it would also swallow whatever auto-pairing did with that terminator +-- — and a pair character is a legal terminator (`\alp(`). One undo +-- restores the same text either way, because the terminator was its own +-- insert to begin with. +-- +-- ONE `buf:replace`: one undo step, one CRDT op, one effective-edit +-- verification. A rejection drops the pending state and does not retry, +-- the same discipline as comment.lua's Q#CT5 and pair.lua. +local function expand(buf, start, span_end, symbol) local cursor_at = symbol:find(CURSOR, 1, true) local text = cursor_at and (symbol:gsub("%$CURSOR", "", 1)) or symbol - local start = p.start_offset + -- The context to compare against AFTER the edit. A buffer intercept + -- may switch window or buffer while the replace runs; the point in + -- whatever it switched to is not ours to move. + local win0 = pmacs.window.current() + local point0 = ed.cursor() + local ok, estart, estop, einserted = pcall(function() return buf:replace(start, span_end, text) end) @@ -188,7 +211,17 @@ local function expand(buf, p, symbol, span_end) -- the new end. Every later self-insert is then silently rejected and -- the editor looks dead. There is no daemon re-grounding that covers -- this; that only holds for an edit that lands at the cursor. - ed.goto_byte(cursor_at and (start + cursor_at - 1) or (start + #text)) + -- + -- Context-guarded exactly as pair.lua's `repair_cursor` is: if the + -- intercept switched us elsewhere, `goto_byte` would move the point + -- of a buffer that has nothing to do with this expansion. + if pmacs.window.current() == win0 and pmacs.window.buffer() == buf then + if cursor_at then + ed.goto_byte(start + cursor_at - 1) + else + ed.goto_byte(translate(point0, estart, estop, einserted)) + end + end return start + #text end @@ -245,6 +278,15 @@ local function on_typed_edit(rec) pending[fid] = nil return false end + -- ...and on a source edit whose context is no longer current. The + -- buffer and window matching is not enough: a redefined self-insert + -- can insert the character and THEN move the point, and expanding + -- over a span the user has left teleports them back into it. Pairing + -- makes the same three-part check for the same reason. + if ed.cursor() ~= rec.post_cursor then + pending[fid] = nil + return false + end local revision do @@ -287,55 +329,114 @@ local function on_typed_edit(rec) p.text = extended p.expected_revision = revision if eager[extended] then - local span_end = p.start_offset + 1 + #extended pending[fid] = nil - expand(buf, p, best[extended].symbol, span_end) + deferred[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = p.start_offset, + text = extended, + symbol = best[extended].symbol, + re_arm = false, + } end -- Claimed either way: an extension that has not yet completed must - -- NOT reach auto-pairing (`\[` in `\[[]]`). + -- NOT reach auto-pairing (`\[` in `\[[]]`), and a completing one is + -- part of the abbreviation, not a character pairing should react to. return true end - -- `ch` does not extend the abbreviation. Expand what is pending - -- FIRST, then let `ch` stand as ordinary text — the terminator is - -- retained, not consumed, and it sits inside the replaced span so the - -- whole thing is one undo step. + -- `ch` does not extend the abbreviation: it TERMINATES it, and a + -- terminator is an ordinary character that auto-pairing is entitled + -- to react to (`\alp(` must give `α()`). So the expansion is + -- DEFERRED to the subscriber below and this returns false, leaving + -- pairing a record whose offsets still describe the buffer. + -- + -- Expanding here and returning false would not do: the replace makes + -- pairing's copy of the record stale, so pairing declines and the + -- closer is silently lost. Expanding here and returning true is + -- worse — it is what shipped in the first revision of this file, and + -- it makes every pair-character terminator silently unpaired. pending[fid] = nil - local hit = best[p.text] - local after - if hit and #p.text > 0 then - -- `span_end` covers the terminator: the leader, the pending text, - -- and `ch`, which has already landed. What replaces it is the - -- symbol followed by `ch` itself. - local span_end = p.start_offset + 1 + #p.text + #ch - after = expand(buf, p, hit.symbol .. ch, span_end) + if best[p.text] and #p.text > 0 then + deferred[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = p.start_offset, + text = p.text, + symbol = best[p.text].symbol, + -- A terminating `\` re-arms as a NEW leader at its own position + -- (`\al\to` → `∀→`). Upstream gets this from `processChange`, + -- where a finished abbreviation reports `isAffected = false` and + -- so does not suppress the new-leader branch. This is NOT the + -- `\\` case: there the pending text is empty, `\` EXTENDS, and + -- the result is one literal backslash with nothing left open. + re_arm = ch == LEADER, + } + elseif ch == LEADER then + -- Nothing to expand, but the leader still opens a fresh + -- abbreviation where it landed. + pending[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = rec.effective_start, + text = "", + expected_revision = revision, + } + return true end - -- A terminating `\` re-arms as a NEW leader at its own position - -- (`\alpha\to` → `α→`). Upstream gets this from `processChange`, - -- where a finished abbreviation reports `isAffected = false` and so - -- does not suppress the new-leader branch. This is not the `\\` case: - -- there the pending text is empty, `\` EXTENDS, and the result is one - -- literal backslash with no pending state left open. - if ch == LEADER then - local start = after and (after - #ch) or rec.effective_start - local ok, rev = pcall(function() return buf:revision() end) - if ok then + return false +end + +-- The deferred expansion, on its own `buffer.after-edit` subscriber. +-- +-- It runs AFTER the whole typed-edit chain — this chunk loads after +-- typed_edit.lua, and hook callbacks run in registration order — so +-- auto-pairing has already reacted to the terminator by the time the +-- expansion rewrites the text in front of it. Pairing's closer lands +-- after the terminator, outside the replaced span, so it survives. +-- +-- It must also run BEFORE lsp.lua's subscriber (Q#AP7): that one +-- flushes `didChange` synchronously on the signature-trigger path, and +-- a server told about `\alp ` instead of `α ` stays wrong until the +-- next edit. This chunk loads before lsp.lua for exactly that reason. +-- +-- A claim by ANY chain consumer stops the chain but not this — which +-- is the point. Pairing claims the terminator it reacts to. +local function run_deferred() + local fid = frontend_id() + if fid == nil then return end + local d = deferred[fid] + deferred[fid] = nil + if not d then return end + + local buf = pmacs.window.buffer() + if not buf or buf ~= d.buffer or pmacs.window.current() ~= d.window then + return + end + + -- The span must still hold exactly what was typed into it. Pairing + -- only edits at the point, which is past this span, so in practice + -- this holds; a buffer intercept is not obliged to be so polite. + local span_end = d.start_offset + 1 + #d.text + local ok, actual = pcall(function() + return buf:slice(d.start_offset, span_end) + end) + if not ok or actual ~= LEADER .. d.text then return end + + local after = expand(buf, d.start_offset, span_end, d.symbol) + if after and d.re_arm then + local rev_ok, rev = pcall(function() return buf:revision() end) + if rev_ok then pending[fid] = { - buffer = rec.buffer, - window = rec.window, - start_offset = start, + buffer = d.buffer, + window = d.window, + start_offset = after, text = "", expected_revision = rev, } end - return true end - - -- Claimed only if an expansion actually happened. Otherwise `ch` is - -- an ordinary character in a Lean buffer and auto-pairing should see - -- it — `\zz` leaves `z` free to pair if it ever were a pair char. - return after ~= nil end -- Q#KR11's seam: a detached frontend's pending state must not outlive @@ -343,8 +444,11 @@ end -- life of the session. pmacs.hook.add("frontend.detached", function(fid) pending[fid] = nil + deferred[fid] = nil end) +pmacs.hook.add("buffer.after-edit", run_deferred) + -- `buffer.after-switch` fires with NO arguments, so it cannot say whose -- switch it was. The acting frontend is the one that produced the most -- recent dispatched input event, which is what `pmacs.frontend.id()` diff --git a/docs/active-work.md b/docs/active-work.md index 034b1fd..f931da1 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -175,7 +175,8 @@ If it does not, stop and repair the remote/fetch configuration. ### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`) -- Framing `docs/lean4-mode-framing.md` **revision 9**, approved. Stage +- Framing `docs/lean4-mode-framing.md` **revision 10** (round 10 = + review of the implementation). Stage 4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b, the Lean content that registers on it. - Footprint: `scripts/regen-lean-abbrev` (new, the generator), @@ -183,7 +184,7 @@ If it does not, stop and repair the remote/fetch configuration. from `leanprover/vscode-lean4@17d1d08`, Apache-2.0), `builtin/runtime/lean_input.lua` (new, the consumer at priority 50), `src/editor.rs` (two `include_str!` blocks), - `tests/lean_input_acceptance.rs` (new, 25 tests), and one + `tests/lean_input_acceptance.rs` (new, 29 tests), and one `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs` (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart from the load sites and that one test. @@ -239,11 +240,31 @@ If it does not, stop and repair the remote/fetch configuration. | `buffer.after-switch` clears every frontend | 1 | | delete the `buffer.after-switch` subscriber | 1 | | `frontend.detached` purges every frontend | 1 | + | claim the terminator | 1 | + | expand inside the chain, then decline | 2 | + | drop the `cursor() == post_cursor` check | 1 | + | place the point without the context guard | 1 | + | load lean_input.lua after lsp.lua | 1 | Acceptance 45f bit by construction: without a registered window for the source frontend it ran six fan-outs with a nil record and proved nothing, because `handle_remote_crdt_op` arms nothing unless the source's active window displays the buffer. +- **Round 10 (review) found three defects, all about what happens + AROUND the expansion rather than about resolving an abbreviation.** A + pair character that TERMINATES an abbreviation never reached pairing + (`\alp(` gave `α(`): the first revision claimed the terminator, and + merely declining is not enough either, because the chain hands each + consumer a copy of the record made before any consumer ran — so + expanding inside the chain invalidates pairing's copy and the closer + is lost anyway (verified by mutation, not assumed). The expansion now + runs on **its own `buffer.after-edit` subscriber** after the chain, + with a span that stops before the terminator. That is a new instance + of Q#AP7, so it is now pinned with the sighelp fake server. + Post-insert point motion was also mistaken for a valid span (the + relevance check needs `cursor() == post_cursor`, as pairing's has + since #110), and cursor placement could move a buffer an intercept + had switched to. - Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED, named in the module header (Q#LN21): six source-peer optimistic inserts replaced by one daemon-peer op. `set_round_trip_input` would diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index 32b1a10..d1dc46b 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -132,7 +132,14 @@ commands, read `docs/active-work.md` immediately after this file. (branch `lean4-stage4b-input-method`, framing rev 9): a vendored 1,855-entry table generated from `leanprover/vscode-lean4@17d1d08` by `scripts/regen-lean-abbrev`, plus a consumer registered on the - Stage 4a chain at priority 50, ahead of pairing. Its durable facts: + Stage 4a chain at priority 50, ahead of pairing. **A consumer + cannot both edit and let a later consumer act on the same + keystroke**: the chain hands each consumer a copy of the record made + before any consumer ran, so an edit invalidates every copy still to + be used. The expansion therefore runs on a SECOND + `buffer.after-edit` subscriber after the chain — which is how a + pair character that terminates an abbreviation still pairs + (`\alp(` → `α()`). Its other durable facts: the table must stay an ORDERED SEQUENCE (equal-length ties resolve by source declaration order, which a `pairs`-iterated map cannot express); a generator round-trip check must re-read the BYTES ON diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 72a83fd..482ad84 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -46,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. Current revision: **9**. +Revision 1 — initial. Current revision: **10**. ### Round 1 (rev 1 → rev 2) @@ -535,6 +535,38 @@ The mechanism (Q#LN11, Q#LN21, Q#LN22) needed no change — these were errors in the examples chosen to pin it, which is why a simulation over the real data found them and four review rounds over the prose did not. +### Round 10 (rev 9 → rev 10) + +Review of the Stage 4b implementation. Three defects in the expander, +all of them about what happens AROUND the expansion rather than about +resolving an abbreviation, plus one stale count. + +1. **A pair character that terminates an abbreviation never reached + auto-pairing.** Q#LN22 already said the terminator is not claimed; + the implementation claimed it whenever an expansion succeeded, so + `\alp(` gave `α(`. Not claiming is necessary and not sufficient — + the chain hands each consumer a copy of the record made before any + consumer ran, so expanding inside the chain invalidates the copy + pairing is holding and the closer is lost anyway. Q#LN22 now + specifies the deferred subscriber and the span that stops before the + terminator; acceptance 45j pins all three failure modes. +2. **Post-insert point motion was mistaken for a valid pending span.** + The relevance check compared buffer and window but not + `ed.cursor() == rec.post_cursor`, so a redefined self-insert that + inserts and then moves the point still expanded — and teleported the + point back. Pairing has made this three-part check since #110. + Acceptance 45k. +3. **Cursor placement could move the wrong buffer.** A buffer intercept + may switch buffers during `buf:replace`; the unguarded `goto_byte` + afterwards moved the switched-to buffer's point. `repair_cursor` is + the precedent. Acceptance 45l. +4. **The coherence census contradicted itself** — nine settings in one + paragraph, eight three paragraphs below. + +Acceptance 45m was added with them: the expansion now runs on its own +`buffer.after-edit` subscriber, which is a new instance of Q#AP7 and +was unpinned. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1718,8 +1750,9 @@ reconstruction of it: - A subsequent self-insert `c` is claimed iff at least one key has `text .. c` as a prefix; then `text = text .. c`. If it is also uniquely-and-completely matching (one of the 1,550), expand now. -- If no key extends `text .. c`, expand `text` **first**, then let `c` - land normally — the chain does *not* claim `c`. +- If no key extends `text .. c`, `c` TERMINATES the abbreviation: the + chain does *not* claim it, and the expansion of `text` is + **deferred** until after the chain has run (round 10; see below). - **A terminating `c` that is itself `\` is then reprocessed as a new leader**, opening a fresh pending abbreviation at its position. This is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6 @@ -1733,6 +1766,37 @@ reconstruction of it: broken by source rank, unmatchable tail appended (`\alp7` → `α7`). - `$CURSOR` is stripped from the symbol and its index becomes the point. +**The expansion is deferred past the chain, and its span stops before +the terminator** (round 10). "Not claiming the terminator" is necessary +and not sufficient: a pair character is a legal terminator (`\alp(` must +give `α()`), and the chain hands every consumer a *copy* of the record +made before any consumer ran. So expanding inside the chain and then +declining leaves auto-pairing holding offsets the replace has already +invalidated — pairing declines and the closer is silently lost, which a +probe confirmed. Claiming the terminator instead suppresses pairing +outright. Neither is recoverable from inside the chain. + +The expander therefore records the pending expansion and performs it on +its **own `buffer.after-edit` subscriber**, registered after +typed_edit.lua's and before lsp.lua's. A claim by any consumer stops the +chain but not a separate subscriber — which is the point, since pairing +claims the terminator it reacts to. The replaced span covers the leader +and the typed text only; whatever pairing did lands after it and +survives untouched. One undo restores the same text either way, because +the terminator was always its own insert. + +Two guards this exposes, both of which pairing already carries: + +- The relevance check is **three-part**, not two: buffer, window, **and + `ed.cursor() == rec.post_cursor`**. A redefined self-insert can insert + the completing character and then move the point, and expanding over a + span the user has left teleports them back into it. +- Cursor placement after the replace is **context-guarded**. A buffer + intercept may switch window or buffer while `buf:replace` runs; an + unguarded `goto_byte` then moves the point of a buffer that has + nothing to do with the expansion. `pair.lua`'s `repair_cursor` is the + precedent. + **Ownership is per frontend, not per buffer** (§2.11). The key is `(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still match `rec.window` for the state to be usable — a frontend that moved @@ -2490,11 +2554,14 @@ criterion 46 requires to stay byte-identical. it assumed `\alpha` takes the finish path when `alpha` is in the 1,550-key eager set (round 9; see 41). - *Finish path.* `\alp` + space yields `α `: the space lands first - and the expansion runs in the following `buffer.after-edit`, so - the terminator is **retained**, not consumed, and it is inside the - replaced span. One undo restores `\alp ` — with its space, not - `\al`. Rev 6 wrote the post-undo text without the terminator, - which would be true only if the terminator were swallowed. + and the expansion runs later in the same `buffer.after-edit` + fan-out, so the terminator is **retained**, not consumed. It sits + OUTSIDE the replaced span, which covers only the leader and the + typed text (round 10) — the observable text and the post-undo + text are the same either way, because the terminator was its own + insert. One undo restores `\alp ` — with its space, not `\al`. + Rev 6 wrote the post-undo text without the terminator, which + would be true only if the terminator were swallowed. - *Eager path.* `\alpha` yields `α` with no terminator typed, and a following space is a **separate** edit. One undo removes the space; a second restores `\alpha`. Asserting the finish-path undo @@ -2598,6 +2665,33 @@ criterion 46 requires to stay byte-identical. `$CURSOR` more than once; - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`, and the tie cases from 45h. +45j. **A pair character that TERMINATES an abbreviation still pairs** + (round 10). `\alp(` yields `α()` with the point between the pair. + Bites three ways, all of which produce different wrong answers: + claiming the terminator gives `α(`; expanding inside the chain and + then declining also gives `α(`, because the replace invalidates the + record copy pairing is holding; and pairing running first gives + `\alp()` unexpanded. Criterion 40 is the same collision from the + other side, and passing it says nothing about this one. +45k. **The relevance check is three-part.** A redefined + `buffer.self-insert` that inserts the completing character and then + moves the point must not expand: `\alph` + `a` under such an + override leaves literal `\alpha` with the point where the command + put it. Bites against checking only buffer and window — the + expansion would otherwise teleport the point back into a span the + user has left. +45l. **Cursor placement is context-guarded.** A buffer intercept that + switches buffers during `buf:replace` must not have the + switched-to buffer's point moved. Bites against an unguarded + `goto_byte`, which translates the LEAN buffer's pre-edit point + through the LEAN buffer's edit and applies it to whatever is + ambient. +45m. **Q#AP7 for the deferred subscriber.** The expansion runs on a + second `buffer.after-edit` subscriber, so it inherits pairing's + flush-ordering obligation: no `didChange` may ever carry the + unexpanded text. Pinned with the `sighelp` fake server and `(` as + the trigger — the flush carrying the terminator carries `α()`. + Falsified by loading lean_input.lua after lsp.lua. 45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` — `f<` and `f>` are both length 2, and `f<` is declared first. Same for `\"` + space → `Ä`, first of eleven equal-length candidates. @@ -2752,7 +2846,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from languages other than Lean, and §4's rule is what keeps them out of a Lean PR. -### 9.1 Coherence impact — stages 4a and 4b (rev 9) +### 9.1 Coherence impact — stages 4a and 4b (rev 10) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 diff --git a/tests/lean_input_acceptance.rs b/tests/lean_input_acceptance.rs index 01ee89e..9270f1b 100644 --- a/tests/lean_input_acceptance.rs +++ b/tests/lean_input_acceptance.rs @@ -8,10 +8,12 @@ use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; use pmacs::editor::EditorState; +use pmacs::lua_bindings::StateDir; use pmacs::protocol::FrontendId; use pmacs::window::{FrontendView, Layout, Window, WindowId}; use std::path::PathBuf; use std::sync::atomic::{AtomicUsize, Ordering}; +use std::time::{Duration, Instant}; fn fresh_dir() -> PathBuf { static SEQ: AtomicUsize = AtomicUsize::new(0); @@ -49,6 +51,10 @@ fn text(s: &EditorState) -> String { String::from_utf8_lossy(&b.as_bytes()).into_owned() } +fn cursor(s: &EditorState) -> i64 { + eval(s, "return pmacs.editor.cursor()") +} + fn type_as(s: &mut EditorState, fid: FrontendId, chars: &str) { for ch in chars.chars() { s.dispatch_key(fid, key(KeyCode::Char(ch))); @@ -176,6 +182,33 @@ fn a_pending_abbreviation_is_never_corrupted_by_auto_pairing() { assert_eq!(text(&s), "⟦⟧", "the full key resolves"); } +#[test] +fn a_pair_character_that_terminates_an_abbreviation_still_pairs() { + // The other half of the collision, and the one the first revision + // of this file got wrong. `(` does not extend `alp`, so it + // TERMINATES — and a terminator is an ordinary character that + // pairing is entitled to react to. + // + // Claiming the terminator suppresses pairing entirely (`α(`). + // Expanding before declining is no better: the replace makes + // pairing's copy of the record stale, so pairing declines and the + // closer is silently lost. Only deferring the expansion past the + // chain gives both. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp("); + assert_eq!( + text(&s), + "α()", + "the abbreviation expanded AND the terminator paired" + ); + assert_eq!( + cursor(&s), + 3, + "and the point sits between the pair — after α (2 bytes) and \ + the opener" + ); +} + #[test] fn a_pair_character_outside_a_pending_abbreviation_still_pairs() { // The other direction: claiming extensions must not disable pairing @@ -271,6 +304,93 @@ fn switching_buffers_clears_pending_state_eagerly() { ); } +#[test] +fn a_self_insert_that_moves_the_point_afterwards_does_not_expand() { + // Buffer and window matching is not enough. A redefined + // `buffer.self-insert` may insert the completing character and THEN + // move the point; expanding over a span the user has left teleports + // them back into it. Pairing makes the same three-part check + // (`ed.cursor() ~= rec.post_cursor`) for the same reason. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alph"); + exec( + &s, + r#" + pmacs.command.unregister("buffer.self-insert") + pmacs.command.define { + name = "buffer.self-insert", + description = "test override: insert, then move the point away", + fn = function(cp) + pmacs.editor.insert_char_over_region(cp) + pmacs.editor.goto_byte(0) + end, + } + "#, + ); + + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "\\alpha", + "the record died with the point that left it — no expansion" + ); + assert_eq!(cursor(&s), 0, "and the point stayed where it was moved to"); +} + +#[test] +fn an_intercept_that_switches_buffers_does_not_move_the_other_points() { + // A buffer intercept may switch window or buffer while the replace + // runs. An unguarded `goto_byte` afterwards moves the point of + // whatever it switched TO — a buffer with nothing to do with this + // expansion. Pairing's `repair_cursor` guards the same way. + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("other.lean"); + std::fs::write(&other, "0123456789").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + exec( + &s, + &format!( + r#" + _G.SWITCHED = false + pmacs.buffer.add_intercept(pmacs.window.buffer(), function(op) + if op.kind == "replace" and not _G.SWITCHED then + _G.SWITCHED = true + pmacs.buffer.find_or_open({od:?}) + end + return nil + end) + "# + ), + ); + + type_str(&mut s, "\\alpha"); + let switched: bool = eval(&s, "return _G.SWITCHED"); + assert!(switched, "the intercept must actually have fired"); + assert_eq!( + text(&s), + "0123456789", + "we are now in the buffer the intercept switched to" + ); + // Whatever point the switch left in that buffer, the expansion must + // not have moved it. Unguarded, `goto_byte` runs against the + // ambient buffer and translates the LEAN buffer's pre-edit point + // (6) through the LEAN buffer's replace, landing at 2 here — a + // number with no meaning in this buffer at all. + assert_eq!( + cursor(&s), + 0, + "its point is untouched — the expansion's cursor placement is \ + guarded on the window and buffer still being the ones it \ + edited" + ); +} + // --------------------------------------------------------------------------- // 44 / 45 — the setting and the language gate, both on the SOURCE buffer // --------------------------------------------------------------------------- @@ -566,6 +686,127 @@ fn the_vendored_table_is_self_consistent() { assert!(!to_eager, "`to` is extended by `top`, `to0`, `toa`, …"); } +// --------------------------------------------------------------------------- +// Q#AP7 for the deferred expansion: it must land before lsp.lua flushes +// --------------------------------------------------------------------------- + +#[test] +fn the_expansion_reaches_the_first_did_change() { + // The expansion runs on its OWN `buffer.after-edit` subscriber, + // after the typed-edit chain. That makes it a new instance of the + // Q#AP7 obligation pairing already carries: lsp.lua's subscriber + // flushes `didChange` SYNCHRONOUSLY on the signature-trigger path, + // and `(` is a trigger. A server told about `\alp(` instead of + // `α()` stays wrong until the next edit — diagnostics, semantic + // tokens and inlay hints all frozen at stale byte positions. + // + // Falsified by loading lean_input.lua after lsp.lua in + // `src/editor.rs`: the expansion would then arrive in the SECOND + // didChange, or not at all. + let dir = fresh_dir(); + let sink = dir.join("changes.jsonl"); + let sink_disp = sink.display().to_string(); + let fake = env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned(); + + let f = dir.join("a.lean"); + std::fs::write(&f, "").unwrap(); + let mut s = EditorState::new(); + s.lua_host.lua().remove_app_data::(); + s.lua_host.lua().set_app_data(StateDir(dir.clone())); + exec(&s, "pmacs.lsp.config = {}"); + exec( + &s, + &format!( + "pmacs.lsp.config.lean4 = {{ + command = '{fake}', + env = {{ + PMACS_FAKE_LSP_MODE = 'sighelp', + PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}', + }}, + }}" + ), + ); + + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + let initialized = "(function() \ + for _,r in ipairs(pmacs.lsp.list()) do \ + if r.state and r.state.kind=='initialized' then return true end \ + end \ + return false \ + end)()"; + assert!(pump_lua_flag(&mut s, initialized, 5), "fake server init"); + + type_str(&mut s, "\\alp("); + assert_eq!(text(&s), "α()", "precondition: the expansion happened"); + + // Wait for the flush that carries the `(` keystroke. Earlier + // keystrokes have already produced their own didChanges, so + // `changes[0]` is NOT the one under test — asserting on it compares + // against `\al` and fails for the wrong reason. + let deadline = Instant::now() + Duration::from_secs(5); + let changes = loop { + s.tick_processes(); + s.tick_lsp(); + s.tick_async(); + let c = did_change_texts(&sink); + if c.iter().any(|t| t.contains('α')) { + break c; + } + assert!( + Instant::now() < deadline, + "no didChange carrying the expansion reached the fake server; got {:?}", + did_change_texts(&sink) + ); + std::thread::sleep(Duration::from_millis(10)); + }; + assert!( + !changes.iter().any(|t| t == "\\alp("), + "no didChange may ever carry the UNEXPANDED text — one would mean lsp.lua flushed before the deferred expansion ran (Q#AP7). Got {changes:?}" + ); + assert_eq!( + changes.last().map(String::as_str), + Some("α()"), + "the flush that carries the terminator carries the expansion and pairing's closer with it" + ); +} + +fn pump_lua_flag(state: &mut EditorState, flag: &str, secs: u64) -> bool { + let deadline = Instant::now() + Duration::from_secs(secs); + loop { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + let done: bool = state + .lua_host + .lua() + .load(format!("return ({flag}) == true")) + .eval() + .unwrap_or(false); + if done { + return true; + } + if Instant::now() >= deadline { + return false; + } + std::thread::sleep(Duration::from_millis(10)); + } +} + +/// The `text` of every `textDocument/didChange` line in the sink, in +/// arrival order. +fn did_change_texts(sink: &std::path::Path) -> Vec { + let Ok(raw) = std::fs::read_to_string(sink) else { + return Vec::new(); + }; + raw.lines() + .filter_map(|l| serde_json::from_str::(l).ok()) + .filter(|v| v.get("method").and_then(|m| m.as_str()) == Some("textDocument/didChange")) + .filter_map(|v| v.get("text").and_then(|t| t.as_str()).map(str::to_owned)) + .collect() +} + // --------------------------------------------------------------------------- // 45i — pending state is per frontend // ---------------------------------------------------------------------------