neuwirth
/
pmacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix(lean4): defer the expansion past the chain, and guard its point 

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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
This commit is contained in:
Levi Neuwirth 2026-07-26 16:47:54 -04:00
parent f8ca722d66
commit f3103a6953
5 changed files with 523 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

192
builtin/runtime/lean_input.lua
View File

@ -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()`

25
docs/active-work.md
View File

@ -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

9
docs/agent-handoff.md
View File

@ -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

112
docs/lean4-mode-framing.md
View File

@ -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

241
tests/lean_input_acceptance.rs
View File

@ -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::<StateDir>();
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<String> {
let Ok(raw) = std::fs::read_to_string(sink) else {
return Vec::new();
};
raw.lines()
.filter_map(|l| serde_json::from_str::<serde_json::Value>(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
// ---------------------------------------------------------------------------