From 3e64898c64dda9beadce028bde65fc3b314d76a3 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 9 Aug 2026 17:11:42 +0200 Subject: [PATCH] docs: record the destination-capture lane as implemented MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Section-local edit to the lane's own block; several lanes edit this file concurrently. Records the two commits, the green gate line (both preservation suites unchanged), the mutation checks that show a matrix of deliberate omissions is not passing vacuously, and the two places the framing did not match the tree: - the rename was 11 references across 5 files, not 8 across 4 — `src/daemon.rs` also calls the capture; - Q#DC-4's "frontend with no document window" is a DEFENSIVE branch. Q#BP6 asserts a layout always keeps a non-side window, with a `debug_assert!` in `non_side_target` that fires under `cargo test`, so a registered frontend in a healthy editor always has a live document window. The decision stands, but #227 should not expect to meet that refusal. Neither changed a decision, and both are recorded rather than quietly absorbed: the framing says "counted, not estimated", and the next reader will check. `ViewDestination`'s own doc comment is corrected in the same commit, because it repeated the framing's over-claim ("a frontend showing only a side window") in the one place a reader would trust it, and `capture_view_destination` now says how reachable its empty pair actually is. Code, not only ledger, since the ledger is not what someone reads when they wonder whether that branch can fire. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai --- docs/active-work.md | 59 ++++++++++++++++++++++++++++++++++++++------- src/editor_core.rs | 14 +++++++++-- 2 files changed, 62 insertions(+), 11 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index ad3f2da..0632278 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -265,7 +265,7 @@ also removed: this branch's "R8 NEEDS A LANE" investigation block, and durable facts are in the retired registry row and the handoff §6 census. -## Destination capture (Q#JR14 generalization) — BRANCHED, framing in review +## Destination capture (Q#JR14 generalization) — IMPLEMENTED, gate green, no PR yet **Written with the lane's first commit**, per the standing correction from #171 and #215. @@ -275,8 +275,46 @@ from #171 and #215. authoritative tip** — the ref, not a SHA. Recover with `git fetch githubsucks && git checkout destination-capture`. -- **Framing `docs/destination-capture-framing.md`, revision 5**, in - review. +- **Framing `docs/destination-capture-framing.md`, revision 5**, + APPROVED after four review rounds. +- **Implemented in two commits.** `779bb02` is the mechanism + (`pmacs.window.capture_destination()`, the `ViewDestination` rename, + the profile argument); `d5a6170` is + `tests/destination_capture_acceptance.rs`, eight pins covering §7. + The full gate line below is green, and both preservation suites pass + **unchanged** (journey 47, dired 31) — no edit to either, which is + §7's stop signal not firing rather than being suppressed. +- **TWO FRAMING CLAIMS THE TREE DID NOT MATCH.** Neither changed a + decision; both are recorded because the framing says "counted, not + estimated" and a reader will check. + 1. **The rename was 11 references across 5 files, not 8 across 4.** + `src/daemon.rs:1804` also calls the capture (the attaching + frontend's directory open), and `editor.rs` holds six references + rather than the counted total. Mechanical either way. + 2. **Q#DC-4's "a frontend with no document window" is a DEFENSIVE + branch, not a routine one.** The obvious spelling — a frontend + showing only a bottom panel — is asserted impossible: Q#BP6 says a + layout always retains at least one non-side window, and + `EditorCore::non_side_target` carries a `debug_assert!` that fires + under `cargo test` when one does. So with Q#BP6 held a *registered* + frontend always has a live document window. The decision still + stands (capture stays total; an adopter with nowhere to land gets a + refusal naming that rather than permission to fall back to ambient + state), and the two Q#DC-4 pins drive the reachable spelling of the + same condition — a layout whose document window has gone while the + view remains. **#227 should not expect to hit this refusal**; it is + insurance, not a path. +- **Mutation-tested, since a matrix of deliberate omissions is exactly + what passes vacuously.** Retyping the profile to `Option` + fails the table and boolean rows with mlua's conversion error (the + number row survives — Lua coerces it — which is why the closed set is + witnessed by more than one non-string). Applying all four checks in + both profiles fails the panel column; applying only check 1 in both + fails the document column. Defaulting an omitted profile to `"panel"` + fails **`journey_acceptance`'s two preservation pins**, which is the + contract claim being executable rather than asserted. Dropping the + frontend scope for the panel profile fails the survives-a-switch pin's + panel row; dropping the no-document-window arm fails the Q#DC-4 pair. - **The public API #227 adopts against (Q#DC-5), pinned so it is a contract rather than an intention:** `pmacs.window.commit_to(dest, body [, profile])`. Profile is an @@ -307,16 +345,19 @@ authoritative tip** — the ref, not a SHA. Recover with and display UI without capturing the initiating frontend (`builtin/runtime/git.lua:609`, `:854`), so a result surfaces in whichever frontend is active when git exits. -- **The mechanism exists but is not Lua-reachable.** - `pmacs.window.commit_to` takes a `DirectoryDestinationLua`, which is +- **The mechanism existed but was not Lua-reachable** until `779bb02`. + `pmacs.window.commit_to` took a `DirectoryDestinationLua`, which is **nonconstructible from Lua** by design (`src/lua_bindings/mod.rs:4256`) and minted only inside the `path.open-directory` listener dispatch (`src/editor.rs:1311`) from a `pub(crate)` capture (`:1241`). So no async Lua continuation outside - a directory open can say where its result belongs. + a directory open could say where its result belongs. Line numbers are + the pre-lane ones, kept because they are what the finding was written + against. - **Scope:** a Lua-reachable capture, a generic rename - (`DirectoryDestination` → `ViewDestination`, 8 references across 4 - files — counted, not estimated), and the preflight question below. + (`DirectoryDestination` → `ViewDestination`; the framing counted 8 + references across 4 files, the tree held **11 across 5** — see the + finding above), and the preflight question below. **No adopter**: git's adoption is #227's work after this lands, since a prerequisite that converts its own first consumer cannot be reviewed separately from it. @@ -335,7 +376,7 @@ authoritative tip** — the ref, not a SHA. Recover with - **Gates, as the executable line rather than a description:** ``` - scripts/gate --acceptance \ + scripts/gate --acceptance destination_capture_acceptance \ --acceptance journey_acceptance \ --acceptance dired_acceptance ``` diff --git a/src/editor_core.rs b/src/editor_core.rs index 0243968..bae3137 100644 --- a/src/editor_core.rs +++ b/src/editor_core.rs @@ -144,8 +144,8 @@ pub enum ResolvedTarget { /// result. /// /// The fields are load-bearing, and the document pair is **optional** -/// (Q#DC-4) because a frontend showing only a side window can still host -/// a panel result: +/// (Q#DC-4) because a panel result needs only a live frontend, so a +/// frontend whose document window has gone can still host one: /// /// * `frontend` — the scope the commit must run in. Always present. /// * `window` — the exact destination; the ambient selected window is @@ -3073,6 +3073,16 @@ impl EditorCore { /// The document pair is set or cleared **together**: a window whose /// entry has gone yields neither half, so no consumer has to handle /// a window without its captured buffer. + /// + /// **How reachable the empty pair is, stated because the framing + /// implies more than the tree does.** Q#BP6 says a frontend layout + /// always retains at least one non-side window, and + /// [`Self::non_side_target`] carries a `debug_assert!` that fires + /// when one does not — so with that invariant held, a *registered* + /// frontend always has a live document window and this branch is + /// **defensive** rather than routine. It stays because the + /// alternative is a capture that can fail, and a caller that can + /// fail is a caller that falls back to ambient state. #[must_use] pub fn capture_view_destination(&self, fid: FrontendId) -> ViewDestination { let pair = self