fix(buffer): make generated buffers survive undo

Review round 2, P1. Undo could empty the "read-only" snapshot.

`render_snapshot` wrote with bypass_intercept, which leaves ordinary
undo history behind, and `Buffer::undo` reaches the rope through
`ensure_writable` without ever consulting the intercept chain. So a
single `C-/` — or `M-x buffer.undo`, which needs no keymap at all —
replaced a freshly rendered snapshot with an empty buffer.
`set_round_trip_input` does not help: it routes the key into the daemon
command path, which is exactly where undo runs.

Rebinding the undo chords buffer-locally would not have closed this,
and `compile.lua` already says so in a comment: "command/menu undo
stays dispatchable". `*compilation*` and listview panels therefore
carry the same latent defect today.

Adds `Buffer::set_generated_contents` (Lua:
`pmacs.buffer.set_generated_contents`): lift `read_only`, replace the
contents skipping intercepts, discard the resulting history, re-assert
`read_only`. This ships the framing's deferred immutability lane as ONE
primitive rather than exposing the setter — a bare `set_read_only`
would let a caller lock a buffer it can no longer refresh, which is
precisely why that lane was deferred. Discarding history is
load-bearing twice: it removes what undo would replay, and it stops a
periodically refreshed buffer accumulating rope clones that `read_only`
guarantees nothing can ever pop.

New acceptance 16c drives the real M-x path
(`command.invoke_interactive`), the chord, and redo, and asserts the
owner's own refresh still works — the operation plain `read_only` would
have broken. Acceptance 16b flips from asserting `is_read_only()` is
false to true, because the property it documented is the one that was
wrong. Three `buffer.rs` unit tests cover the primitive directly,
including that ten refreshes leave an empty undo stack.

Bite: restoring the delete+insert render reproduces the report exactly
— `left: Some("")` against the full snapshot — failing 16c and 16b.

Still open, and now named in the framing, COHERENCE.md §14 and the
ledger: `*compilation*` and listview have not adopted the primitive and
remain emptiable by `M-x buffer.undo`; a streaming-friendly variant is
needed for the append case. In CRDT mode `read_only` is what refuses
undo, since loro's UndoManager exposes no clear through `CrdtState`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
This commit is contained in:
Levi Neuwirth 2026-07-26 13:12:08 -04:00
parent b9fbb42dc0
commit 8c5b39ef32
7 changed files with 306 additions and 17 deletions

View File

@ -1214,7 +1214,16 @@ Primitive-by-primitive against the list above:
rebindable (§6's counter-example). rebindable (§6's counter-example).
- **Output channel** ✓ — the compile-mode `*compilation*` model - **Output channel** ✓ — the compile-mode `*compilation*` model
(streamed, intercept-read-only, error-rule parsing), reused by grep (streamed, intercept-read-only, error-rule parsing), reused by grep
and shell-command. and shell-command. **Caveat found in terminal copy mode's review
(Stage 2): "intercept-read-only" is not read-only.** `Buffer::undo`
reaches the rope through `ensure_writable` without consulting the
intercept chain, so `M-x buffer.undo` empties such a buffer — and
rebinding the undo *chords* buffer-locally does not close it, as
`compile.lua`'s own comment admits ("command/menu undo stays
dispatchable"). `Buffer::set_generated_contents` (write + discard
history + assert `read_only`, in one authorized call) now fixes this
for the terminal snapshot; `*compilation*` and listview panels have
not yet adopted it and remain emptiable.
- **Diagnostics collection** ✓ — `DiagnosticStore` + signs + unified - **Diagnostics collection** ✓ — `DiagnosticStore` + signs + unified
`error.next` source. `error.next` source.
- **Transient selector** ✓ — the minibuffer (though its `source` - **Transient selector** ✓ — the minibuffer (though its `source`

View File

@ -319,12 +319,18 @@ end
-- drift between the two. -- drift between the two.
local function render_snapshot(record) local function render_snapshot(record)
local text = raw_copy_retained(record.terminal) or "" local text = raw_copy_retained(record.terminal) or ""
local buf = record.buffer -- The owner-authorized write, and the ONLY one this buffer accepts.
local len = buf:len() --
-- Snapshot writes bypass the read-only intercept; everything else is -- Not `delete`+`insert` with `bypass_intercept` (review round 2): that
-- rejected by it. -- leaves the buffer writable at the rope, and it leaves undo history
if len > 0 then buf:delete(0, len, { bypass_intercept = true }) end -- behind. `Buffer::undo` reaches the rope through `ensure_writable`
if #text > 0 then buf:insert(0, text, { bypass_intercept = true }) end -- without consulting the intercept chain, so a single `C-/` — or
-- `M-x buffer.undo`, which no buffer-local rebinding can take away —
-- replaced a freshly rendered snapshot with an empty buffer.
-- `set_generated_contents` writes, discards the history, and leaves
-- `read_only` asserted, so undo/redo and remote CRDT imports are all
-- refused at the rope.
pmacs.buffer.set_generated_contents(record.buffer, text)
end end
local function claim_snapshot(term_buf) local function claim_snapshot(term_buf)

View File

@ -738,6 +738,39 @@ If it does not, stop and repair the remote/fetch configuration.
18a *and* 18b; restoring name-keyed identity fails 18b; making 18a *and* 18b; restoring name-keyed identity fails 18b; making
`render_snapshot` a no-op fails **both** 18 and 19 (the vacuity, `render_snapshot` a no-op fails **both** 18 and 19 (the vacuity,
demonstrated); and forcing the view off the tail fails 20. demonstrated); and forcing the view off the tail fails 20.
- **Review round 2 — one P1, and its fix retires half a named deferral.**
**Undo emptied the "read-only" snapshot.** `render_snapshot` wrote with
`bypass_intercept`, leaving ordinary undo history, and **`Buffer::undo`
reaches the rope through `ensure_writable` without ever consulting the
intercept chain** — so `C-/` *or* `M-x buffer.undo` replaced a freshly
rendered snapshot with an empty buffer. `set_round_trip_input` does not
help: it routes the key into the daemon command path, which is where
undo runs.
- **Rebinding the undo chords would NOT have fixed it**, and
`compile.lua` already says so in a comment — "command/menu undo stays
dispatchable". `*compilation*` and listview panels therefore carry the
same latent defect today.
- Fixed with `Buffer::set_generated_contents` (Lua
`pmacs.buffer.set_generated_contents`): lift `read_only`, replace
skipping intercepts, **discard history**, re-assert `read_only`. This
ships the deferred lane's two halves *as one primitive* — a bare
`set_read_only` would let a caller lock a buffer it can no longer
refresh, which is exactly why that lane was deferred. Clearing history
also stops a periodically refreshed buffer accumulating rope clones
nothing can ever pop.
- New pins: **acc16c** drives the real M-x path
(`command.invoke_interactive`), the chord, and redo, and asserts the
owner's refresh still works; **acc16b** flipped from asserting
`is_read_only()` is *false* to *true*, because the property it
described is the one that was fixed; plus three `buffer.rs` unit tests.
- Bite: restoring the `delete`+`insert` render reproduces the report
exactly — `left: Some("")` against the full snapshot — failing acc16c
and acc16b.
- **Still open:** `*compilation*` and listview remain emptiable by
`M-x buffer.undo`; the primitive they need now exists and is proven,
so the remainder is adoption plus a streaming-friendly variant. In
CRDT mode `read_only` is what refuses undo, since loro's `UndoManager`
exposes no clear through `CrdtState`.
- Load-bearing decisions, each forced by scouted ground truth: - Load-bearing decisions, each forced by scouted ground truth:
- profiles are a **raw Lua table**`ConfigValue` is four scalars with - profiles are a **raw Lua table**`ConfigValue` is four scalars with
no table kind, so they join `pmacs.lsp.config` / `pmacs.pair.sets`; no table kind, so they join `pmacs.lsp.config` / `pmacs.pair.sets`;

View File

@ -508,6 +508,35 @@ additive, on its own binding, and does not replace scroll-and-select.
"skip the intercepts". Naming only the setter would have made it look like a "skip the intercepts". Naming only the setter would have made it look like a
one-line follow-up. one-line follow-up.
**PARTIALLY RETIRED in Stage 2, because review round 2 turned it from a
nice-to-have into a defect.** An intercept guards the dispatch path only,
and `Buffer::undo` reaches the rope through `ensure_writable` without ever
consulting the intercept chain — so a single `C-/` replaced a freshly
rendered snapshot with an empty buffer. Rebinding the undo chords
buffer-locally, which is `*compilation*`'s existing idiom, does **not**
close it: `compile.lua` says so itself ("command/menu undo stays
dispatchable"), and `M-x buffer.undo` needs no keymap.
The fix ships the deferral's two halves together as **one** primitive
rather than exposing the setter: `Buffer::set_generated_contents` (Lua:
`pmacs.buffer.set_generated_contents`) lifts `read_only`, replaces the
contents skipping intercepts, **discards the history**, and re-asserts
`read_only`. Pairing the lock with the write is precisely what makes it
safe — a bare `set_read_only` would let a caller lock a buffer it can no
longer refresh, which is why the lane was deferred in the first place.
Discarding history is load-bearing twice: it removes the entries undo
would replay, and it stops a periodically refreshed buffer accumulating
rope clones that `read_only` guarantees nothing can ever pop.
**What remains of the lane:** `*compilation*` and listview panels still
rely on intercept-plus-round-trip and are still emptiable by
`M-x buffer.undo`. The primitive they need now exists and is proven, so
the remaining work is adoption plus a streaming-friendly variant
(`*compilation*` appends rather than replacing wholesale). The CRDT half
is also still open: `set_generated_contents` clears the v0.1 stacks, and
in CRDT mode `read_only` is what refuses undo, since loro's
`UndoManager` has no clear exposed through `CrdtState`.
## Acceptance ## Acceptance
### Stage 1 — `terminal-config` ### Stage 1 — `terminal-config`
@ -577,6 +606,15 @@ additive, on its own binding, and does not replace scroll-and-select.
them for selection copy. them for selection copy.
15. isearch over the snapshot finds content that is **only in scrollback** 15. isearch over the snapshot finds content that is **only in scrollback**
(scrolled off the visible screen), with no change to `src/search.rs` (B1). (scrolled off the visible screen), with no change to `src/search.rs` (B1).
16c. **Undo cannot empty the snapshot, by chord OR by command** (review
round 2). `Buffer::undo` bypasses the intercept chain entirely, so the
snapshot must be `read_only` at the rope. Pinning only the chords would
be a false pass: `M-x buffer.undo` and the menu reach the command with
no keymap involved, which is why `*compilation*`'s chord-rebinding idiom
does not close this. Pinned through **`invoke_interactive`**, the real
M-x path, plus the chord, plus redo — and paired with an assertion that
the owner's own refresh still works, since that is what plain
`read_only` would have broken.
16. **Ungated, runs in CI:** focusing the snapshot buffer makes 16. **Ungated, runs in CI:** focusing the snapshot buffer makes
`dispatch_idle_for` report **false**. This is the whole mechanism Q#TC6a `dispatch_idle_for` report **false**. This is the whole mechanism Q#TC6a
depends on, it needs no CRDT, and it fails the moment depends on, it needs no CRDT, and it fails the moment

View File

@ -504,6 +504,55 @@ impl Buffer {
self.read_only = read_only; self.read_only = read_only;
} }
/// Replace a generated buffer's entire contents on behalf of its owner,
/// and leave it genuinely immutable.
///
/// This is the **owner-authorized update path** that genuine
/// immutability for generated buffers requires. A snapshot, panel or
/// `*compilation*` buffer must reject ordinary edits, **undo, redo**,
/// and remote CRDT imports alike — and only [`read_only`] does that.
/// An edit intercept is not enough: it guards the dispatch/edit path
/// only, while [`Buffer::undo`] reaches the rope through
/// `ensure_writable` without ever consulting the intercept chain. A
/// buffer protected by an intercept alone can therefore be emptied by
/// `C-/`, by `M-x buffer.undo`, or by the menu — the command is
/// reachable even where the chords are rebound to no-ops.
///
/// But `read_only` also blocks the owner's own refresh, which is the
/// operation such buffers exist for. So the owner needs exactly one
/// door, and this is it: lift the flag, replace the contents skipping
/// intercepts, **discard the resulting history**, re-assert the flag.
///
/// Discarding history is not tidiness. Without it every refresh pushes
/// undo entries holding full rope clones that nothing can ever pop —
/// `read_only` guarantees they are unreachable — so a periodically
/// refreshed buffer would grow without bound.
///
/// [`read_only`]: Self::set_read_only
pub fn set_generated_contents(&mut self, bytes: &[u8]) -> Result<(), BufferError> {
self.read_only = false;
let result = self.replace_whole_buffer(bytes);
// Cleared even on failure: a partial replace must not leave a
// half-applied edit reachable through an undo the owner cannot see.
self.undo.clear();
self.redo.clear();
self.read_only = true;
result
}
fn replace_whole_buffer(&mut self, bytes: &[u8]) -> Result<(), BufferError> {
let len = self.len();
if len > 0 {
self.apply_edit_skip_intercepts(EditOp::Delete {
range: Range::new(0, len),
})?;
}
if !bytes.is_empty() {
self.apply_edit_skip_intercepts(EditOp::Insert { pos: 0, bytes })?;
}
Ok(())
}
fn ensure_writable(&self) -> Result<(), BufferError> { fn ensure_writable(&self) -> Result<(), BufferError> {
if self.read_only { if self.read_only {
Err(BufferError::ReadOnly { Err(BufferError::ReadOnly {
@ -1955,6 +2004,72 @@ mod tests {
} }
); );
/// The whole point of the primitive: after an owner write the buffer
/// is immutable, and `undo` — which never consults the intercept
/// chain — cannot reach back past it.
#[test]
fn set_generated_contents_writes_then_locks_and_leaves_nothing_to_undo() {
let mut buf = Buffer::new(BufferId::next(), "*generated*");
buf.set_generated_contents(b"first render").expect("write");
assert_eq!(buf.len(), 12);
assert!(buf.is_read_only(), "the buffer ends immutable");
assert!(
matches!(buf.undo(), Err(BufferError::ReadOnly { .. })),
"undo must be refused at the rope, not merely at dispatch"
);
assert!(matches!(buf.redo(), Err(BufferError::ReadOnly { .. })));
// Even with the lock lifted there is no history to replay — the
// protection does not depend on the flag alone.
buf.set_read_only(false);
assert!(matches!(buf.undo(), Err(BufferError::NothingToUndo)));
assert!(matches!(buf.redo(), Err(BufferError::NothingToRedo)));
}
/// Refreshing repeatedly must not accumulate unreachable history.
/// Each render would otherwise push entries holding full rope clones
/// that `read_only` guarantees nothing can ever pop.
#[test]
fn repeated_generated_writes_do_not_accumulate_history() {
let mut buf = Buffer::new(BufferId::next(), "*generated*");
for i in 0..10 {
buf.set_generated_contents(format!("render {i}").as_bytes())
.expect("write");
}
let mut bytes = vec![0u8; buf.len() as usize];
buf.snapshot_rope().slice(0, buf.len(), &mut bytes);
assert_eq!(String::from_utf8(bytes).expect("utf8"), "render 9");
buf.set_read_only(false);
assert!(
matches!(buf.undo(), Err(BufferError::NothingToUndo)),
"ten renders must leave an empty undo stack, not ten entries"
);
}
/// An ordinary edit is still refused after a generated write, so the
/// primitive does not quietly leave the buffer writable.
#[test]
fn set_generated_contents_still_refuses_ordinary_edits() {
let mut buf = Buffer::new(BufferId::next(), "*generated*");
buf.set_generated_contents(b"content").expect("write");
assert!(matches!(
buf.apply_edit(EditOp::Insert {
pos: 0,
bytes: b"x"
}),
Err(BufferError::ReadOnly { .. })
));
assert!(matches!(
buf.apply_edit_skip_intercepts(EditOp::Insert {
pos: 0,
bytes: b"x"
}),
Err(BufferError::ReadOnly { .. })
));
}
#[cfg(feature = "crdt")] #[cfg(feature = "crdt")]
#[test] #[test]
fn read_only_rejects_remote_crdt_before_import_and_allows_empty_bootstrap() { fn read_only_rejects_remote_crdt_before_import_and_allows_empty_bootstrap() {

View File

@ -3065,6 +3065,29 @@ fn install_buffer_module(lua: &Lua, registry: &SharedRegistry) -> mlua::Result<T
)?; )?;
} }
{
let reg = registry.clone();
buffer.set(
// Replace a generated buffer's contents and leave it genuinely
// immutable — the one authorized door through `read_only`.
//
// Deliberately NOT an exposed `set_read_only`: that would let a
// caller lock a buffer with no way to refresh it, which is the
// failure mode that kept generated-buffer immutability deferred.
// Pairing the lock with the write in a single call is what makes
// it safe to ship.
"set_generated_contents",
lua.create_function(move |_, (id, text): (BufferIdLua, mlua::String)| {
let mut registry = reg.borrow_mut();
let buffer = registry.get_mut(id.0).map_err(mlua::Error::external)?;
buffer
.set_generated_contents(&text.as_bytes())
.map_err(mlua::Error::external)?;
Ok(())
})?,
)?;
}
{ {
let reg = registry.clone(); let reg = registry.clone();
buffer.set( buffer.set(

View File

@ -333,10 +333,10 @@ fn acc16_dispatch_idle_is_false_while_the_snapshot_is_focused() {
} }
/// Acceptance 16 (the other half): the intercept rejects ordinary edits, /// Acceptance 16 (the other half): the intercept rejects ordinary edits,
/// and — the fact that makes round-trip load-bearing rather than defence /// and the buffer is genuinely `read_only` at the rope boundary, so the
/// in depth — the buffer is **not** `read_only` at the rope boundary. /// protection does not depend on which key or command was used.
#[test] #[test]
fn acc16b_the_intercept_rejects_edits_but_is_not_rope_level_protection() { fn acc16b_the_snapshot_is_immutable_at_the_rope_not_merely_intercepted() {
let mut state = EditorState::new(); let mut state = EditorState::new();
let terminal = open_fill_terminal(&mut state); let terminal = open_fill_terminal(&mut state);
focus_terminal(&state, terminal); focus_terminal(&state, terminal);
@ -347,10 +347,6 @@ fn acc16b_the_intercept_rejects_edits_but_is_not_rope_level_protection() {
let after = buffer_text_by_name(&state, SNAPSHOT_NAME).expect("snapshot"); let after = buffer_text_by_name(&state, SNAPSHOT_NAME).expect("snapshot");
assert_eq!(before, after, "the read-only intercept rejects self-insert"); assert_eq!(before, after, "the read-only intercept rejects self-insert");
// Q#TC6a, stated as a test so the next reader does not mistake the
// intercept for real immutability: no Lua binding sets
// `Buffer::read_only`, so this buffer accepts rope/CRDT mutation and
// only the round-trip mark above keeps a replica from producing one.
let core = state.core.borrow(); let core = state.core.borrow();
let registry = core.registry.borrow(); let registry = core.registry.borrow();
let ids = registry.ids(); let ids = registry.ids();
@ -364,18 +360,87 @@ fn acc16b_the_intercept_rejects_edits_but_is_not_rope_level_protection() {
}) })
.expect("snapshot buffer id"); .expect("snapshot buffer id");
assert!( assert!(
!registry registry
.get(snapshot) .get(snapshot)
.expect("snapshot buffer") .expect("snapshot buffer")
.is_read_only(), .is_read_only(),
"the Lua intercept does NOT set Buffer::read_only — this is why \ "an intercept guards the dispatch path only; `Buffer::undo` reaches \
set_round_trip_input is the guard and not hardening" the rope through `ensure_writable` without consulting it, so the \
snapshot must be read-only at the rope"
); );
drop(registry); drop(registry);
drop(core); drop(core);
state.process_supervisor.borrow_mut().shutdown(); state.process_supervisor.borrow_mut().shutdown();
} }
/// Acceptance 16c (review round 2, P1): **undo cannot empty the snapshot**,
/// through the chord *or* through the command.
///
/// The chord half alone would be a false pass. `M-x buffer.undo` and the
/// menu reach `Buffer::undo` without passing through any buffer-local
/// keymap, so rebinding `C-/` to a no-op — the existing `*compilation*`
/// idiom, which documents that "command/menu undo stays dispatchable" —
/// leaves the buffer emptiable. Only rope-level `read_only` closes both.
#[test]
fn acc16c_undo_cannot_empty_the_snapshot_by_chord_or_by_command() {
let mut state = EditorState::new();
let terminal = open_fill_terminal(&mut state);
focus_terminal(&state, terminal);
exec(&state, "pmacs.terminal.copy_mode(TERM_BUF)");
let rendered = buffer_text_by_name(&state, SNAPSHOT_NAME).expect("snapshot");
assert!(
rendered.contains("LINE200"),
"precondition: the snapshot has content to lose"
);
// The command path — reachable regardless of any buffer-local binding.
let _: Value = state
.lua_host
.lua()
.load(r"return pcall(pmacs.command.invoke_interactive, 'buffer.undo')")
.eval()
.expect("invoke_interactive is callable");
assert_eq!(
buffer_text_by_name(&state, SNAPSHOT_NAME).as_deref(),
Some(rendered.as_str()),
"M-x buffer.undo must not empty the snapshot"
);
// The chord path.
press(&mut state, KeyCode::Char('/'), KeyModifiers::CONTROL);
assert_eq!(
buffer_text_by_name(&state, SNAPSHOT_NAME).as_deref(),
Some(rendered.as_str()),
"C-/ must not empty the snapshot"
);
// Redo is the same door.
let _: Value = state
.lua_host
.lua()
.load(r"return pcall(pmacs.command.invoke_interactive, 'buffer.redo')")
.eval()
.expect("invoke_interactive is callable");
assert_eq!(
buffer_text_by_name(&state, SNAPSHOT_NAME).as_deref(),
Some(rendered.as_str()),
"buffer.redo must not alter the snapshot either"
);
// ...and the owner's own refresh still works, which is the whole
// reason plain `read_only` was not enough on its own.
emit_into_child(&mut state, terminal, "STILLREFRESHES");
exec(&state, "pmacs.terminal.copy_mode(TERM_BUF)");
assert!(
buffer_text_by_name(&state, SNAPSHOT_NAME)
.expect("snapshot")
.contains("STILLREFRESHES"),
"the owner-authorized write path must survive immutability"
);
state.process_supervisor.borrow_mut().shutdown();
}
/// Acceptance 18: re-invoking refreshes in place, and the lifecycle runs /// Acceptance 18: re-invoking refreshes in place, and the lifecycle runs
/// both directions. /// both directions.
#[test] #[test]