Revision 7 of `docs/destination-capture-framing.md`, closing the
correctness blocker review found in `0efc8c0` and the smaller
reachability hole beside it.
THE BLOCKER. The `"panel"` commit profile skipped preflight checks 2-4
on the claim that a panel result never touches a document window. That
claim is false: panel placement FALLS BACK to an ordinary document
window when the frontend is not `panel_capable` or its one side slot is
dedicated elsewhere -- `apply_placement` says so in its own comment --
and then installs the result there. So a `"panel"` commit could replace
a NEWER document with every stale-intent guard skipped: capture A, the
user opens B, the continuation lands, B is gone. That is the exact
failure `commit_to` exists to prevent, reached through the profile
meant to be the safe one.
WHY NOT A PREFLIGHT PREDICTION. Revision 6 proposed predicting the
fallback at preflight, arguing nothing could change in between because
the body cannot `await`. Refusing `await` prevents another COROUTINE
interleaving; it places no restriction on the body itself, which is
arbitrary Lua running synchronously and can invalidate the snapshot in
two statements -- take the panel, set it `dedicated`, then request a
side display. No preflight predicate closes that, however phrased: the
measurement is taken before the thing it measures is decided.
WHAT THIS DOES INSTEAD. `EditorCore::display_buffer` refuses between
`resolve_placement` and `apply_placement` when a side request resolved
to `PlacementKind::Ordinary` under an active `"panel"` contract whose
destination fails the document preconditions. That is the first moment
the fallback is a fact rather than a guess, and refusing before
`apply_placement` means a refused fallback mutates nothing. The
contract rides on the core, installed and restored by the same
`ScopedFrontendGuard` that scopes the frontend, so a profile can never
outlive the body that declared it; the field is crate-private, so Lua
cannot claim a profile for a placement it did not commit to.
The preflight predicate SURVIVES as an early refusal and not as the
guarantee. `panel_placement_can_fall_back` still gates the relaxation
in `commit_destination_refusal`, so the statically knowable case -- a
frontend that cannot render a panel at all, and will not acquire the
capability mid-body -- refuses before the body allocates a buffer,
registers a handle and paints. That is the same reason `commit_to`
preflights at all. Both layers are pinned, and neither pin subsumes the
other.
The four document checks now live once, in
`EditorCore::document_destination_refusal`: they are evaluated from two
sites, and two hand-written copies is how a backstop ends up weaker
than the thing it backs.
THREE DELIBERATE LIMITS, each a different decision rather than a
stricter version of this one. The document profile is untouched --
re-running its checks at placement would newly refuse dired's own
documented panel path, which is a preservation-suite stop signal. Only
a fallback is guarded, not every `Ordinary` placement -- a `"panel"`
body calling `display_file` is pinned as succeeding. And the refusal is
of the PLACEMENT, not of falling back: a `"panel"` commit with an
intact destination still degrades gracefully into the document window,
because turning graceful degradation into an error would regress every
consumer that works today on a frontend without panel capability.
THE SECOND HOLE. `commit_profile` did `name.to_str()?`, but Lua strings
are BYTE strings, so a `string.char(255)` profile hit mlua's generic
UTF-8 conversion error before `BAD_COMMIT_PROFILE` was ever
constructed -- the same reachability class as the `Option<String>`
defect revision 5 fixed, one layer down. The comparison is on bytes
now, and the invalid-UTF-8 row joins the number/table/boolean rows
asserting on message content.
FOUR DOC SITES repeated the false claim (`ViewDestination`'s own doc
twice, `capture_view_destination`, `ViewDestinationLua`) and are
corrected. Nothing else relied on it: dired, the only Lua `commit_to`
consumer, takes the two-argument document profile and already had all
four checks; `compile.lua`'s `already_in_panel` queries live state; and
the terminal adopter's rollback keys off `created_side`, already false
on a fallback.
Tests: 12 pins, up from 8. Three carry the enforcement split and none
subsumes another -- the pre-established fallback (both causes, the body
must not run), the inside-the-body transition (the body runs, the
result must not land), and the graceful fallback (a valid destination
still lands). Mutation-checked four ways; the pattern of which rows
survive each mutation is in `docs/active-work.md`.
`journey_acceptance` (47) and `dired_acceptance` (31) pass UNCHANGED.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
`docs/destination-capture-framing.md` §7, eight tests.
The one that decides the lane is `the_preflight_matrix_holds_in_both
_profiles`. Every cell Q#DC-2 marks "not applicable" for the panel
profile is asserted as NOT refusing, not merely left untested: a check
deliberately omitted and a check someone forgot look identical from the
outside, and the next reader restores the second one. The document
column re-asserts all four refusals in the same table, so a mutation
that collapses the two profiles fails one column or the other.
`a_bad_profile_is_refused_by_one_message_that_names_the_accepted_values`
is the guard on the argument's TYPE, not only on its behaviour. It
asserts the number, table and boolean cases produce the same message as
an unrecognized string --- which stops being true the moment the
argument is retyped to `Option<String>`, because mlua then rejects the
value during argument conversion and the pointed message is never
reached.
`a_captured_destination_survives_a_frontend_switch` runs under both
profiles. The panel profile drops three of the four preflight checks,
and a plausible way to implement that is to drop the frontend scope with
them --- which would leave a panel continuation resolving its target
from ambient state, the exact defect the lane removes.
`a_two_argument_commit_takes_the_document_profile` witnesses the default
through a check the panel profile omits (a stale buffer), because
asserting merely that a legacy call does not error would pass on one
silently downgraded to the panel profile.
ONE FINDING, RECORDED IN THE TEST RATHER THAN WORKED AROUND. Q#DC-4's
"a frontend with no document window" reads as a frontend showing only a
bottom panel, and that state is asserted impossible: Q#BP6 says a layout
always retains at least one non-side window, and `non_side_target`
carries a `debug_assert!` that fires under `cargo test` if one ever
does. So with Q#BP6 held, a registered frontend in a healthy editor
always has a live document window, and the absent document pair is a
DEFENSIVE branch rather than a routine one. The decision still stands
--- capture stays total, and an adopter with nowhere to land gets a
refusal naming that rather than permission to guess --- 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. The helper says
so at its definition.
`tests/journey_acceptance.rs` (47) and `tests/dired_acceptance.rs` (31)
pass UNCHANGED, which is §7's stop signal and the reason the profile
default is the document one.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
Levi Neuwirth