fix(window): refuse the mutation that would invalidate a panel commit
Revision 8 of `docs/destination-capture-framing.md`, replacing the
revision-7 design at `ca72461`, plus the invalid-UTF-8 profile hole.
The framing now carries §3's enumeration, performed.
THE BLOCKER, unchanged. The `"panel"` commit profile skips preflight
checks 2-4 on the claim that a panel result never touches a document
window. Panel placement FALLS BACK into an ordinary document window
when the frontend is not `panel_capable` or its one side slot is
dedicated elsewhere, and installs the result there --- so a `"panel"`
commit could replace a NEWER document with every stale-intent guard
skipped.
TWO REJECTED SHAPES, kept in the framing as the record of why not
those. Revision 6 predicted the fallback at preflight and argued the
body could not change it; false, because refusing `await` stops another
COROUTINE interleaving, not the body's own synchronous statements.
Revision 7 (`ca72461`) moved enforcement to the placement boundary;
that breaks the invariant `commit_to` exists for --- `docs/agent-handoff.md`
requires it to preflight BEFORE the callback, because a body creates
buffers, handles and paint long before it asks to display anything, so
"validating at display time is four mutations too late". A refusal
arriving after all of that is a partial commit with an error return.
REVISION 8 DOES NEITHER. The preflight stays exactly where it was, and
the mutations that would invalidate it are REFUSED AT THE ATTEMPT ---
the same shape as `Handle:await` being refused inside a commit scope,
for the identical reason: something that would invalidate the scope's
guarantee is rejected outright rather than predicted around or caught
late. With them refused, the fallback never comes into existence.
THE ENUMERATION, PERFORMED --- this is the load-bearing part, and it is
closed for a structural reason rather than because inspection ran out
of ideas. Full working in the framing §3.
`resolve_placement` reaches `Ordinary` from a side request through
exactly two branches, so only two pieces of state are levers at all:
`panel_capable`, and the one side window's `dedicated`.
`panel_capable` is UNREACHABLE from a body: written only where a
`FrontendView` is constructed, and nothing in `src/lua_bindings/`
constructs, registers or unregisters one --- `register_frontend_view`
has callers only in `daemon.rs` and core unit tests.
`dedicated` has eight writes. Five are reachable: `apply_placement`'s
`Side` created, replacing and non-replacing arms, and `set_params`. Two
`Ordinary` arms are harmless --- every `Ordinary` target is filtered
`!is_side`, and one only ever clears the flag. One is a unit test.
Closing the side window is NOT a route, checked rather than assumed:
with no side leaf `side_window_for` returns `None` and placement
CREATES a fresh panel instead of falling back. `panel_hidden` is not
consulted by placement, and `params.side` is unreachable.
`quit_window`'s `QuitAction::Restore { dedicated: true }` is
UNREACHABLE, and this was the surprise --- it looked like a route with
no `dedicated` argument at the call site at all. `Restore` is stored
only on a REPLACING side placement, and a dedicated slot can never be
the target of one: a side request with a different buffer falls through
to `Ordinary`, and an exact-target request is refused by
`window_accepts_buffer`. Guarded anyway, labelled defensive, because
its unreachability is emergent from two rules in another function.
GUARDS SITED WHERE THE PROPERTY CONVERGES. All three `Side` arms are
reached through `apply_placement`, which has EXACTLY ONE caller --- so
one guard in `display_buffer` covers every request-driven dedication,
including spellings that do not exist yet. `set_params` is a genuinely
separate write and is guarded separately; dedication does NOT converge
before the field itself, and that is stated rather than papered over.
`Window::params.dedicated` is a public field, so the compiler does not
enforce the funnel --- the acceptance rows are what would catch a new
direct writer.
WHAT IS DELIBERATELY NOT REFUSED. The document profile is untouched:
constraining its body would newly refuse dired's own documented panel
path, a preservation-suite stop signal. Dedicating a DOCUMENT window is
still allowed, since it cannot change which of panel-or-document a side
request resolves to. And falling back is still allowed --- a frontend
that cannot render a panel degrades gracefully exactly as today,
because this refuses the mutation that MANUFACTURES a fallback, never
the fallback itself.
THE SECOND HOLE. `commit_profile` did `name.to_str()?`, but Lua strings
are BYTE strings, so `string.char(255)` hit mlua's generic UTF-8 error
before `BAD_COMMIT_PROFILE` was constructed --- the same reachability
class as the `Option<String>` defect revision 5 fixed, one layer down.
Bytes now, with the row asserting on message content.
TESTS: 12 pins. The inside-the-body test is ONE ROW PER REACHABLE WRITE
SITE, not per call spelling, because one spelling reaches three
different writes: `set_params`, and `display{side, dedicated}` in each
of the created, replacing and non-replacing arms. Each asserts the
three things revision 8 requires --- the dedication call is refused, the
slot is still undedicated afterwards, and nothing partial was installed
(no `*result*` buffer, panel unchanged, document unchanged).
Mutation-checked per guard: deleting the `display_buffer` guard fails
all three display rows, verified INDIVIDUALLY by rotating each to the
front so the first failure cannot mask the rest; deleting the
`set_params` guard fails only that row.
THREE FRAMING CORRECTIONS ride along, all of them cases of the document
teaching something it later argues against. Section 3 stated the
disproved premise unconditionally --- "the panel case would inherit a
check about a window it never touches" --- a hundred lines before
correcting it, so a reader met the wrong claim first; it is now
qualified at the point of the claim, and section 2 carried the same
unconditional form one section earlier ("it lands in the bottom panel")
and now says it REQUESTS one. The handoff citation was written "section
748" twice when it is LINE 748, and this document's authority is that
its citations can be followed. And the "not asserted exhaustive" hedge
on the route list is retired: the enumeration is closed structurally,
because `resolve_placement` reaches `Ordinary` from a side request
through exactly two branches.
`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
This commit is contained in:
parent
ccbed7ab55
commit
2fc2985029
|
|
@ -265,13 +265,13 @@ 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) — revision 8 OPEN; the shipped code implements the REJECTED revision 7
|
||||
## Destination capture (Q#JR14 generalization) — revision 8 IMPLEMENTED, gate green, no PR yet
|
||||
|
||||
**DO NOT PREPARE A PR, AND DO NOT READ THE SHIPPED DESIGN AS CORRECT.**
|
||||
The mechanism landed at `0efc8c0`; review found a correctness blocker;
|
||||
`ca72461` implements **revision 7**, which review then **also
|
||||
rejected**. Framing **revision 8** is the current design and is **not
|
||||
implemented**.
|
||||
`ca72461` implemented **revision 7**, which review then **also**
|
||||
rejected; the commit below replaces it with **revision 8** and its
|
||||
§3 enumeration is **performed and recorded in the framing**. No PR — the
|
||||
lane was told not to open one.
|
||||
|
||||
**The original blocker:** the panel profile skipped checks 2–4 on the
|
||||
claim that a panel result never touches a document window. **Panel
|
||||
|
|
@ -297,14 +297,42 @@ re-learning:**
|
|||
refused inside a commit scope: the fallback never comes into
|
||||
existence, and refusal stays mutation-free on `(false, reason)`.
|
||||
|
||||
**The enumeration is the load-bearing part, and it is NOT complete.**
|
||||
Dedication is reachable by at least two routes — `set_params`, and
|
||||
`display(buf, { side = …, dedicated = true })`, which writes
|
||||
`request.dedicated` into the side window (`src/editor_core.rs:4535`).
|
||||
The second was found in review *after* the first was specified, which
|
||||
is the evidence that guarding one named call site is not a design.
|
||||
**Every discovered route must be recorded here and carry its own
|
||||
acceptance row.**
|
||||
**THE ENUMERATION IS THE LOAD-BEARING PART, AND IT IS NOW CLOSED — for
|
||||
a structural reason, not because inspection ran out of ideas.** Full
|
||||
working in the framing §3; the short form:
|
||||
|
||||
- **Only two pieces of state can matter**, because `resolve_placement`
|
||||
reaches `Ordinary` from a side request through exactly two branches:
|
||||
`panel_capable`, and the one side window's `dedicated`.
|
||||
- **`panel_capable` is unreachable from a body.** It is written only
|
||||
where a `FrontendView` is constructed, and nothing in
|
||||
`src/lua_bindings/` constructs, registers or unregisters one —
|
||||
`register_frontend_view` has callers only in `daemon.rs` and core
|
||||
unit tests.
|
||||
- **Eight writes to `dedicated` exist** (`rg 'params\.dedicated\s*='
|
||||
src/`); **five are reachable**: `apply_placement`'s `Side` created /
|
||||
replacing / non-replacing arms, and `set_params`. Two `Ordinary` arms
|
||||
are harmless (their target is never a side window; one only ever
|
||||
clears the flag) and one is a unit test.
|
||||
- **The guards are sited where the property converges, not per caller.**
|
||||
All three `Side` arms are reached through `apply_placement`, which has
|
||||
**exactly one caller** — so one guard in `display_buffer` covers every
|
||||
request-driven dedication, including spellings that do not exist yet.
|
||||
`set_params` is a genuinely separate write and is guarded separately;
|
||||
dedication does **not** converge before the field itself, and that is
|
||||
stated rather than papered over.
|
||||
- **Closing the side window is NOT a route**, checked rather than
|
||||
assumed: with no side leaf `side_window_for` returns `None` and
|
||||
placement **creates** a fresh panel instead of falling back. Hiding is
|
||||
likewise irrelevant — `panel_hidden` is not consulted by placement.
|
||||
- **`quit_window`'s `QuitAction::Restore { dedicated: true }` is
|
||||
UNREACHABLE**, and this was the surprise. `Restore` is stored only on
|
||||
a *replacing* side placement, and a dedicated slot can never be the
|
||||
target of one. Guarded anyway, labelled defensive, because its
|
||||
unreachability is emergent from two rules in another function.
|
||||
- **What this does not rule out:** the enumeration is closed over the
|
||||
current tree, not future edits. `params.dedicated` is a public field,
|
||||
so nothing but the acceptance rows would catch a new direct writer.
|
||||
|
||||
**Also closed:** an invalid-UTF-8 profile (`string.char(255)`) reached
|
||||
`to_str()` and surfaced mlua's generic conversion error instead of the
|
||||
|
|
@ -320,53 +348,61 @@ 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 7.**
|
||||
Revisions 1–5 were approved over four review rounds; revisions 6 and 7
|
||||
are corrections carrying the blocker above, and **revision 7's design
|
||||
is what the tree implements** — revision 6's preflight prediction is
|
||||
NOT the shipped mechanism and must not be restored from that document.
|
||||
- **Framing `docs/destination-capture-framing.md`, revision 8.**
|
||||
Revisions 1–5 were approved over four review rounds; revisions 6, 7
|
||||
and 8 are corrections carrying the blocker above, and **revision 8's
|
||||
design is what the tree implements**. Revisions 6 and 7 are described
|
||||
in that document as the record of why *not* those; neither is in the
|
||||
tree and neither should be restored from it.
|
||||
- **Implemented in three commits.** `779bb02` is the mechanism
|
||||
(`pmacs.window.capture_destination()`, the `ViewDestination` rename,
|
||||
the profile argument); `d5a6170` is
|
||||
`tests/destination_capture_acceptance.rs`; the revision-7 commit is
|
||||
`tests/destination_capture_acceptance.rs`; the revision-8 commit is
|
||||
the panel-profile correction plus the invalid-UTF-8 hole. **12 pins**,
|
||||
and both preservation suites pass **unchanged** (journey 47, dired 31)
|
||||
— §7's stop signal not firing rather than being suppressed.
|
||||
- **HOW THE PANEL PROFILE IS ENFORCED, so revision 6's version does not
|
||||
get reinstated by someone reading only that document.**
|
||||
- `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
|
||||
(`fallback_commit_refusal`). Refusing there means a refused fallback
|
||||
mutates nothing.
|
||||
- **HOW THE PANEL PROFILE IS ENFORCED, in one sentence so no earlier
|
||||
revision gets reinstated by someone reading only that document:** the
|
||||
preflight stays exactly where it was, and the mutations that would
|
||||
invalidate it are **refused at the attempt**.
|
||||
- `EditorCore::panel_commit_dedication_refusal` is the one rule. It
|
||||
fires while a `"panel"` `CommitContract` is on the core for this
|
||||
frontend, and is consulted from `display_buffer` (before
|
||||
`apply_placement`, so a refused attempt mutates nothing),
|
||||
`pmacs.window.set_params` (before its borrow, so `fixed_rows` in the
|
||||
same table is not applied either), and `quit_window`.
|
||||
- **This is the same shape as `Handle:await` being refused inside a
|
||||
commit scope**, and for the identical reason: something that would
|
||||
invalidate the scope's guarantee is rejected outright rather than
|
||||
predicted around or caught late.
|
||||
- The contract (`CommitContract { destination, profile }`) rides on
|
||||
the core, installed and restored by the **same** `ScopedFrontendGuard`
|
||||
that scopes the frontend, so a `"panel"` profile can never outlive
|
||||
the body that declared it. The field is private to the crate — Lua
|
||||
cannot claim a profile for a placement it did not commit to.
|
||||
- **The preflight predicate survives as an EARLY REFUSAL, 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
|
||||
separately and neither test subsumes the other.
|
||||
- **`panel_placement_can_fall_back` remains the preflight**, unchanged
|
||||
in role: it measures whether this frontend places side requests in
|
||||
the panel *right now*. With the invalidating mutations refused, that
|
||||
measurement stays true for the life of the body, which is what makes
|
||||
it a guarantee rather than a forecast.
|
||||
- The four document checks live once, in
|
||||
`EditorCore::document_destination_refusal`, because they are now
|
||||
evaluated from two sites and two hand-written copies is how a
|
||||
backstop ends up weaker than the thing it backs.
|
||||
`EditorCore::document_destination_refusal`.
|
||||
- **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 — a preservation-suite stop signal); only a
|
||||
**fallback** is guarded, not every `Ordinary` placement (a `"panel"`
|
||||
body calling `display_file` is pinned as succeeding by
|
||||
`a_captured_destination_survives_a_frontend_switch`); 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.
|
||||
(constraining its body would newly refuse dired's own documented
|
||||
panel path — a preservation-suite stop signal); **dedicating a
|
||||
document window is still allowed** (it cannot change which of
|
||||
panel-or-document a side request resolves to); and **falling back is
|
||||
still allowed** — a frontend that cannot render a panel degrades
|
||||
gracefully exactly as today, because this refuses the mutation that
|
||||
*manufactures* a fallback, never the fallback itself.
|
||||
- **Mutation-checked per guard, and the pattern is the evidence the rows
|
||||
are independent rather than one assertion repeated.** Deleting the
|
||||
`display_buffer` guard fails the three `display{side, dedicated}` rows
|
||||
— verified **individually**, by rotating each to the front of the
|
||||
table, since the first failure otherwise masks the rest. Deleting the
|
||||
`set_params` guard fails only that row and leaves the display rows
|
||||
passing. Both leave every other test in the file green.
|
||||
- **Audit: nothing else relied on "a panel never touches a document".**
|
||||
Four doc sites repeated the claim (`ViewDestination`'s own doc twice,
|
||||
`capture_view_destination`, `ViewDestinationLua`) and were corrected;
|
||||
|
|
@ -409,23 +445,26 @@ authoritative tip** — the ref, not a SHA. Recover with
|
|||
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.
|
||||
|
||||
**Revision 7's four, each isolating a different way to get it wrong** —
|
||||
and the pattern of *which* rows survive each is the evidence the layers
|
||||
**Revision 8's four, each isolating a different way to get it wrong** —
|
||||
and the pattern of *which* rows survive each is the evidence the parts
|
||||
are independent rather than redundant:
|
||||
1. delete the `fallback_commit_refusal` call from `display_buffer` →
|
||||
**only** the inside-the-body pin fails. Every other test passes,
|
||||
which is exactly the hole revision 6 would have shipped.
|
||||
2. delete the `panel_placement_can_fall_back` arm from
|
||||
1. delete the `panel_commit_dedication_refusal` call from
|
||||
`display_buffer` → the three `display{side, dedicated}` rows fail,
|
||||
**verified individually** by rotating each to the front of the
|
||||
table so the first failure cannot mask the rest. Every other test
|
||||
passes — which is exactly the hole an implementation guarding only
|
||||
`set_params` would ship.
|
||||
2. delete it from `set_params` → **only** that row fails; the three
|
||||
display rows still pass.
|
||||
3. delete the `panel_placement_can_fall_back` arm from
|
||||
`commit_destination_refusal` → **only** the two pre-established
|
||||
fallback rows fail, and they fail on shape (a raise from the
|
||||
backstop, with the body having run) rather than on outcome.
|
||||
3. make `panel_placement_can_fall_back` unconditionally `true` (the
|
||||
fallback rows fail, which is the preflight half.
|
||||
4. make `panel_placement_can_fall_back` unconditionally `true` (the
|
||||
"widen the predicate" non-fix) → the really-lands-in-the-panel pin,
|
||||
the Q#DC-4 panel pin and the matrix's three panel rows all fail.
|
||||
That is the profiles collapsing into one, made visible.
|
||||
4. make `fallback_commit_refusal` refuse *every* panel fallback → only
|
||||
the graceful-degradation pin fails, which is the guard
|
||||
over-reaching.
|
||||
That is the two profiles collapsing into one, made visible — the
|
||||
named fallback design, showing up as a test diff rather than
|
||||
silently.
|
||||
|
||||
And reverting the byte comparison to `to_str()?` fails the
|
||||
`invalid utf-8` row with mlua's conversion error, on content.
|
||||
|
|
|
|||
|
|
@ -1,8 +1,11 @@
|
|||
# A destination capture any async continuation can use
|
||||
|
||||
**Status: revision 8. The mechanism is implemented at `0efc8c0`;
|
||||
revisions 6–8 carry an OPEN correctness blocker that is NOT yet
|
||||
implemented.**
|
||||
**Status: revision 8. The mechanism is implemented at `0efc8c0`; the
|
||||
correctness blocker revisions 6–8 carry is IMPLEMENTED, in revision 8's
|
||||
shape, with §3's enumeration performed and recorded below.** Revisions
|
||||
6 and 7 proposed fixes that review rejected; **neither is in the tree**,
|
||||
and the two paragraphs describing them are kept as the record of why
|
||||
this shape and not those.
|
||||
|
||||
*(Revisions 2–5 said "Pre-implementation. Awaiting approval" while the
|
||||
ledger recorded the lane as approved and implemented. Same
|
||||
|
|
@ -12,13 +15,14 @@ standing in its own header.)*
|
|||
**Revision 8 rejects BOTH of the previous two fixes and takes a third
|
||||
shape.** Revision 6 predicted the fallback at preflight (the body can
|
||||
change it). Revision 7 moved enforcement to the placement boundary —
|
||||
which **breaks the invariant `commit_to` exists for**: handoff §748
|
||||
says it preflights *before* the callback because "validating at display
|
||||
time is four mutations too late", so a placement-time refusal arrives
|
||||
after arbitrary Lua has created buffers, handles and paint. Revision 8
|
||||
keeps the preflight and **refuses the mutations that would invalidate
|
||||
it**, the same shape as the existing await refusal. Refusal stays
|
||||
mutation-free on the `(false, reason)` path.
|
||||
which **breaks the invariant `commit_to` exists for**:
|
||||
`docs/agent-handoff.md:748` says it preflights *before* the callback
|
||||
because "validating at display time is four mutations too late", so a
|
||||
placement-time refusal arrives after arbitrary Lua has created buffers,
|
||||
handles and paint. Revision 8 keeps the preflight and **refuses the
|
||||
mutations that would invalidate it**, the same shape as the existing
|
||||
await refusal. Refusal stays mutation-free on the `(false, reason)`
|
||||
path.
|
||||
|
||||
**Revision 6 fixes an UNSOUND matrix, not a preference.** Q#DC-2 gave
|
||||
the panel profile only check 1, on the claim that a panel result never
|
||||
|
|
@ -137,8 +141,11 @@ that was declined for the `scripts/gate` repair, for the same reason.
|
|||
the finding that shapes the design:
|
||||
- `*git-status*` goes through `listview.open`, which resolves
|
||||
`display` with a **`"panel"`** default
|
||||
(`builtin/runtime/listview.lua:550`). It lands in the bottom
|
||||
panel, **not** in a document window.
|
||||
(`builtin/runtime/listview.lua:550`). It **requests** the bottom
|
||||
panel rather than a document window — *requests*, because a side
|
||||
request FALLS BACK into a document window on a frontend that is not
|
||||
`panel_capable` or whose one slot is dedicated elsewhere. That
|
||||
fallback is this lane's blocker; §3 and Q#DC-2 carry it.
|
||||
- `*git-diff*` calls `pmacs.window.display(buf, { select = true })`
|
||||
— the **document** target, deliberately, "so the status panel it
|
||||
was invoked from stays visible beside it"
|
||||
|
|
@ -152,11 +159,25 @@ loses to the user**"* — a user who replaced the buffer while work was
|
|||
in flight is newer information than the request.
|
||||
|
||||
**That predicate is right for a document replacement and wrong for a
|
||||
panel.** The git status panel does not replace the captured window's
|
||||
buffer; it opens in the bottom panel beside it. Refusing to show it
|
||||
because the user switched files in the document window would be a
|
||||
refusal with no relationship to what the continuation actually does —
|
||||
the panel case would inherit a check about a window it never touches.
|
||||
panel — WHILE THE PANEL REALLY IS A PANEL, which is the qualification
|
||||
the rest of this document exists to add.** A git status panel that
|
||||
lands in the bottom panel does not replace the captured window's
|
||||
buffer; it opens beside it. Refusing to show it because the user
|
||||
switched files in the document window would be a refusal with no
|
||||
relationship to what the continuation actually does, and that case
|
||||
would inherit a check about a window it never touches.
|
||||
|
||||
**Read the previous paragraph with its condition attached, not as a
|
||||
standing fact.** Panel placement **falls back** into an ordinary
|
||||
document window when the frontend is not `panel_capable` or its one
|
||||
side slot is dedicated elsewhere — and then the panel case *does* touch
|
||||
the captured window, replacing whatever the user put there. That
|
||||
fallback is this lane's correctness blocker, and the unqualified
|
||||
version of this claim is precisely what made revision 5's matrix
|
||||
unsound. The resolution is below, at the end of Q#DC-2: the preflight
|
||||
measures whether this frontend places side requests in the panel, and
|
||||
the mutations that would falsify that measurement mid-commit are
|
||||
refused.
|
||||
|
||||
Meanwhile the diff case *is* a document replacement, and wants exactly
|
||||
the dired semantics.
|
||||
|
|
@ -298,7 +319,7 @@ dedicate the side slot itself.
|
|||
|
||||
Revision 7 then moved enforcement to the placement boundary. **That
|
||||
breaks the invariant `commit_to` exists for.** `docs/agent-handoff.md`
|
||||
§748 states it without qualification:
|
||||
`docs/agent-handoff.md:748` states it without qualification:
|
||||
|
||||
> [`commit_to`] preflights every precondition *before* invoking the
|
||||
> callback — dired mutates handle state, `prev`, and paint long before
|
||||
|
|
@ -326,9 +347,11 @@ than aspirational:**
|
|||
- `panel_capable` has **no Lua binding at all** — checked across
|
||||
`src/lua_bindings/`. A body cannot make a frontend panel-incapable.
|
||||
|
||||
**AT LEAST TWO ROUTES REACH DEDICATION, and the second was found in
|
||||
review after the first was specified — which is the evidence that
|
||||
guarding one named call site is not a design:**
|
||||
**FIVE WRITES REACH DEDICATION.** Review found the second *after* the
|
||||
first was specified, which is the evidence that guarding one named call
|
||||
site is not a design — and the enumeration below, performed against the
|
||||
tree rather than by recall, found three more. The two review named
|
||||
first are:
|
||||
|
||||
1. **`set_params`** — the writable-field path (`window_panel.rs:888`).
|
||||
2. **`display(buf, { side = …, dedicated = true })`** — writes
|
||||
|
|
@ -338,21 +361,82 @@ guarding one named call site is not a design:**
|
|||
guarding only route 1 passes revision 8's test while keeping the
|
||||
original defect.**
|
||||
|
||||
**The implementation must ENUMERATE every body-reachable transition,
|
||||
record each one here, and give each reachable route its own acceptance
|
||||
row.** Closing the side window, or any other path to "no usable side
|
||||
slot", counts. The two above are what review has found so far and are
|
||||
**not** asserted to be exhaustive — a third would not be surprising,
|
||||
and finding it is part of the work rather than a later review's job.
|
||||
This is the discipline `gate-protocol-build` applied to Q#GR-1: the
|
||||
fact the design rests on gets observed, not assumed.
|
||||
**THE ENUMERATION, PERFORMED. It is CLOSED, and it is closed for a
|
||||
structural reason rather than by inspection stopping when it ran out of
|
||||
ideas.** Recorded here as the framing required, with what was looked
|
||||
for, what was found, and what cannot be ruled out.
|
||||
|
||||
**If the enumeration turns out to be open-ended**, the fallback is to
|
||||
*Step 1 — how few pieces of state can matter.* `resolve_placement`
|
||||
reaches `Ordinary` from a side request through exactly two branches, so
|
||||
only two pieces of state are levers at all: `FrontendView::panel_capable`,
|
||||
and the one side window's `Window::params.dedicated`. Everything else a
|
||||
body can touch is irrelevant by construction, which is what makes the
|
||||
enumeration finite instead of "every mutation in the editor".
|
||||
|
||||
*Step 2 — `panel_capable` is unreachable, not merely unguarded.* It is
|
||||
written **only** where a `FrontendView` is constructed, and no
|
||||
`FrontendView` is constructed, registered or unregistered anywhere in
|
||||
`src/lua_bindings/` — `register_frontend_view` and
|
||||
`unregister_frontend_view` have callers only in `daemon.rs` (attach and
|
||||
detach) and in core unit tests. A body cannot reach it.
|
||||
|
||||
*Step 3 — every write to `dedicated`, from `rg 'params\.dedicated\s*='
|
||||
src/`, classified.* Eight sites, no exceptions:
|
||||
|
||||
| # | site | verdict |
|
||||
|---|---|---|
|
||||
| 1 | `apply_placement`, `Side` **created** | reachable — `display{side, dedicated}` with no panel yet |
|
||||
| 2 | `apply_placement`, `Side` **replacing** | reachable — `display{side, dedicated}`, different buffer |
|
||||
| 3 | `apply_placement`, `Side` **non-replacing** | reachable — `display{side, dedicated}`, same buffer |
|
||||
| 4 | `apply_placement`, `Ordinary` (`!fell_back`) | harmless — every `Ordinary` target is filtered `!is_side`, so it is never the slot |
|
||||
| 5 | `apply_placement`, `Ordinary` (clear) | harmless — only ever writes `false` |
|
||||
| 6 | `set_params` | reachable — the direct write (Q#BP2c) |
|
||||
| 7 | `quit_window`, `QuitAction::Restore` | **unreachable**, see below |
|
||||
| 8 | an `EditorCore` unit test | not Lua-reachable |
|
||||
|
||||
*Step 4 — the guards, sited where the property converges rather than at
|
||||
each caller.* Sites 1, 2, 3 (and 4, 5) are all reached through
|
||||
`apply_placement`, which has **exactly one caller**, `display_buffer`.
|
||||
So one guard there covers every request-driven dedication, including
|
||||
routes that do not exist yet. `set_params` is a genuinely separate write
|
||||
and is guarded separately — dedication does *not* converge before the
|
||||
field itself, and that is stated rather than papered over. Two live
|
||||
guards, five reachable sites.
|
||||
|
||||
*Step 5 — what was looked for and found NOT to be a route.* Closing the
|
||||
side window is **not** one: with no side leaf `side_window_for` returns
|
||||
`None` and `resolve_placement` **creates** a fresh panel rather than
|
||||
falling back, so quitting or hiding the panel mid-commit is safe, and
|
||||
`panel_hidden` is not consulted by placement at all. `params.side` is
|
||||
likewise unreachable — `set_params` refuses it and only
|
||||
`apply_placement`'s created branch writes it, so a body cannot promote
|
||||
an already-dedicated document window into the slot.
|
||||
|
||||
*Step 6 — site 7 is unreachable, and this is the one finding that
|
||||
surprised.* `QuitAction::Restore` carries the outgoing `dedicated` flag,
|
||||
so quitting the panel looked like a route with no `dedicated` argument
|
||||
at the call site at all. It cannot be constructed: `Restore` is only
|
||||
ever *stored* on a **replacing** side placement, and a dedicated slot
|
||||
can never be the target of one — a side request with a different buffer
|
||||
falls through to `Ordinary`, and an exact-target request is refused by
|
||||
`window_accepts_buffer`. So `Restore { dedicated: true }` has no
|
||||
producer. It is guarded anyway, defensively and labelled as such,
|
||||
because its unreachability is an emergent property of two rules in a
|
||||
different function.
|
||||
|
||||
**What this does NOT rule out.** The enumeration is closed over the
|
||||
current tree, not over future edits: relaxing `resolve_placement`'s
|
||||
dedicated arm, or adding a binding that writes `params.dedicated`
|
||||
directly, reopens it. `Window::params.dedicated` is a public field, so
|
||||
the compiler does not enforce the funnel — the acceptance rows are what
|
||||
would catch a regression, one per reachable site.
|
||||
|
||||
**If the enumeration had turned out open-ended**, the fallback was to
|
||||
**collapse the two profiles** — run all four checks always, losing the
|
||||
panel relaxation. That is safe, simple, and honest; it is not the
|
||||
preferred answer only because it makes the parameterization pointless.
|
||||
Choosing it is a design decision needing its own approval, not a
|
||||
silent retreat.
|
||||
silent retreat. **It was not needed.**
|
||||
|
||||
**What is NOT the fix: refusing a panel commit that would fall back.**
|
||||
Falling back to an ordinary window is existing, deliberate behaviour
|
||||
|
|
@ -531,9 +615,12 @@ incidental: no arguments is what keeps capture profile-blind.
|
|||
Three assertions, and the second and third are the ones that matter:
|
||||
the dedication call itself is **refused**; the side slot is **still
|
||||
undedicated afterwards**; and no partial result was installed.
|
||||
**One row per route** (§3): `set_params`, and the
|
||||
`display{side, dedicated = true}` option path. A single row against
|
||||
one route is what would let the other keep the defect. The
|
||||
**One row per reachable WRITE SITE** (§3), which is four and not two:
|
||||
`set_params`, and `display{side, dedicated}` in each of
|
||||
`apply_placement`'s **created**, **replacing** and **non-replacing**
|
||||
arms. A single row against one route is what would let another keep
|
||||
the defect — and rows per *call spelling* would have missed that one
|
||||
spelling reaches three different writes. The
|
||||
two bullets above cannot catch this — both establish their fallback
|
||||
state *before* `commit_to` is entered, so a preflight-snapshot design
|
||||
passes them.
|
||||
|
|
|
|||
|
|
@ -3488,6 +3488,23 @@ impl EditorCore {
|
|||
}
|
||||
other => other,
|
||||
};
|
||||
// Q#DC-2 (revision 8). A `Restore` carries the OUTGOING
|
||||
// presentation's `dedicated` flag (see `apply_placement`), so
|
||||
// quitting the panel can re-dedicate the one slot without any
|
||||
// `dedicated` argument appearing at the call site. Refused for
|
||||
// the same reason and at the same point as the other attempts —
|
||||
// before `quit_window` has touched anything.
|
||||
if let QuitAction::Restore {
|
||||
dedicated: true, ..
|
||||
} = action
|
||||
&& self
|
||||
.windows
|
||||
.get(&target)
|
||||
.is_some_and(crate::window::Window::is_side)
|
||||
&& let Some(reason) = self.panel_commit_dedication_refusal(fid)
|
||||
{
|
||||
return Err(format!("window.quit: {reason}"));
|
||||
}
|
||||
match action {
|
||||
QuitAction::Delete => {
|
||||
// Capture the remembered origin BEFORE the window dies:
|
||||
|
|
@ -4029,10 +4046,19 @@ impl EditorCore {
|
|||
.ok_or_else(|| format!("frontend {fid:?} has no window layout"))?
|
||||
.active;
|
||||
let placement = self.resolve_placement(fid, request)?;
|
||||
// THE PLACEMENT BOUNDARY (Q#DC-2, revision 7). Refuse before
|
||||
// `apply_placement` so a refused fallback mutates nothing.
|
||||
if let Some(reason) = self.fallback_commit_refusal(request, &placement) {
|
||||
return Err(reason);
|
||||
// Q#DC-2 (revision 8): dedicating the side slot inside a
|
||||
// `"panel"` commit is refused AT THE ATTEMPT, so the preflight's
|
||||
// measurement cannot go stale. `resolve_placement` is pure, so
|
||||
// this still refuses before anything is mutated.
|
||||
//
|
||||
// Note the guard is on the DEDICATION, not on the display: the
|
||||
// body's ordinary `display(buf, {side = "bottom"})` is exactly
|
||||
// what a panel continuation is for and always proceeds.
|
||||
if request.dedicated == Some(true)
|
||||
&& matches!(placement.kind, PlacementKind::Side { .. })
|
||||
&& let Some(reason) = self.panel_commit_dedication_refusal(fid)
|
||||
{
|
||||
return Err(format!("display: {reason}"));
|
||||
}
|
||||
self.apply_placement(fid, request, &placement)?;
|
||||
let select = request
|
||||
|
|
@ -4207,62 +4233,97 @@ impl EditorCore {
|
|||
}
|
||||
|
||||
/// **The guarantee** behind the `"panel"` commit profile (Q#DC-2,
|
||||
/// revision 7): a side request that actually fell back into a
|
||||
/// document window must satisfy the document preconditions.
|
||||
/// revision 8): inside such a commit, the operations that would make
|
||||
/// this frontend's side request fall back are **refused at the
|
||||
/// attempt**.
|
||||
///
|
||||
/// Reaching [`PlacementKind::Ordinary`] while a side was REQUESTED is
|
||||
/// exactly the fallback [`Self::apply_placement`] documents — not
|
||||
/// panel-capable, or the one slot is dedicated elsewhere — and the
|
||||
/// result is then installed into a **document** window. A `"panel"`
|
||||
/// commit that skipped checks 2–4 on the strength of "a panel never
|
||||
/// touches a document window" would, right here, replace a document
|
||||
/// view with no stale-intent guard at all: capture A, the user opens
|
||||
/// B, the continuation lands, B is gone. That is the failure
|
||||
/// `commit_to` exists to prevent, arrived at through the profile
|
||||
/// meant to be the safe one.
|
||||
/// # The defect this closes
|
||||
///
|
||||
/// **Why here and not at preflight.** This is the first moment the
|
||||
/// fallback is a *fact*. A preflight snapshot cannot bind it: the
|
||||
/// body is arbitrary synchronous Lua and may create the very
|
||||
/// condition — take the panel, set it `dedicated`, then ask for a
|
||||
/// side — after the snapshot was taken. Refusing `await` inside the
|
||||
/// commit scope stops a *second coroutine* interleaving; it places no
|
||||
/// restriction on the body's own statements.
|
||||
/// The panel profile skips preflight checks 2–4 on the strength of "a
|
||||
/// panel result never touches a document window". Panel placement
|
||||
/// **falls back** into an ordinary document window when the frontend
|
||||
/// is not `panel_capable` or its one side slot is dedicated elsewhere
|
||||
/// ([`Self::apply_placement`] says so in its own comment), and then
|
||||
/// installs the result there. So a `"panel"` commit that reached a
|
||||
/// fallback would replace a document view with no stale-intent guard:
|
||||
/// capture A, the user opens B, the continuation lands, B is gone.
|
||||
///
|
||||
/// Three deliberate limits, each of which would be a different
|
||||
/// decision rather than a stricter version of this one:
|
||||
/// # Why this shape, and not the two that were tried first
|
||||
///
|
||||
/// * **The document profile is untouched.** Its preflight already ran
|
||||
/// these checks against the same destination, and re-running them
|
||||
/// here would newly refuse dired's own panel path, which documents
|
||||
/// and accepts the fallback (`builtin/runtime/dired.lua`).
|
||||
/// * **Only a fallback, not every document placement.** A panel-profile
|
||||
/// body that displays into a document window *without asking for a
|
||||
/// side* has mislabelled its profile; it has not exercised this
|
||||
/// relaxation. Widening to every [`PlacementKind::Ordinary`] would
|
||||
/// also refuse a `"panel"` commit whose body calls `display_file`,
|
||||
/// which is pinned as succeeding.
|
||||
/// * **Refusing the placement, not the fallback.** Falling back is
|
||||
/// deliberate graceful degradation for a frontend without panel
|
||||
/// capability; a `"panel"` commit whose destination is still valid
|
||||
/// falls back and lands exactly as it does today. The profile
|
||||
/// relaxes checks; it does not get to move where a result goes.
|
||||
fn fallback_commit_refusal(
|
||||
&self,
|
||||
request: &DisplayRequest,
|
||||
placement: &Placement,
|
||||
) -> Option<String> {
|
||||
if request.side.is_none() || !matches!(placement.kind, PlacementKind::Ordinary) {
|
||||
return None;
|
||||
}
|
||||
/// * **Predicting the fallback at preflight is unsound.** The body is
|
||||
/// arbitrary *synchronous* Lua and can create the condition itself.
|
||||
/// Refusing `await` inside the commit scope stops a second
|
||||
/// coroutine interleaving; it places no restriction on the body's
|
||||
/// own statements.
|
||||
/// * **Refusing at the placement boundary is too late.** `commit_to`
|
||||
/// preflights *before* invoking the callback precisely because a
|
||||
/// body creates buffers, registers handles and paints long before
|
||||
/// it asks to display anything — "validating at display time is
|
||||
/// four mutations too late" (`docs/agent-handoff.md`). A refusal
|
||||
/// arriving after all of that is not a refusal; it is a partial
|
||||
/// commit with an error return.
|
||||
///
|
||||
/// So the preflight stays where it is and **the mutation that would
|
||||
/// invalidate it is rejected** — the same shape as `Handle:await`
|
||||
/// being refused inside a commit scope, for the identical reason.
|
||||
/// With these refused, the preflight measurement cannot go stale, the
|
||||
/// fallback never comes into existence, and nothing needs refusing
|
||||
/// late.
|
||||
///
|
||||
/// # The enumeration this rests on
|
||||
///
|
||||
/// [`Self::resolve_placement`] can only reach
|
||||
/// [`PlacementKind::Ordinary`] from a side request in two ways, so
|
||||
/// only two pieces of state matter:
|
||||
///
|
||||
/// 1. `FrontendView::panel_capable` is false. It is written **only**
|
||||
/// where a `FrontendView` is constructed, and no `FrontendView` is
|
||||
/// constructed, registered or unregistered anywhere in
|
||||
/// `src/lua_bindings/` — that is the daemon's attach path. **A
|
||||
/// body cannot reach it at all.**
|
||||
/// 2. The frontend's one side slot exists **and is dedicated** to a
|
||||
/// different buffer. `Window::params.dedicated` is the only
|
||||
/// remaining lever, and every write to it is guarded or harmless:
|
||||
/// the two in `apply_placement`'s `Ordinary` arm target a document
|
||||
/// window (never a side one — every `Ordinary` target is filtered
|
||||
/// `!is_side`) and one of them only ever clears the flag; the
|
||||
/// three in its `Side` arm and the one in `pmacs.window.set_params`
|
||||
/// are the attempts refused here; and `quit_window` restoring a
|
||||
/// saved `dedicated: true` presentation is refused too.
|
||||
///
|
||||
/// **Losing the side window is NOT a route** and was checked rather
|
||||
/// than assumed: with no side leaf, `side_window_for` returns `None`
|
||||
/// and `resolve_placement` **creates** a fresh panel instead of
|
||||
/// falling back. Closing or hiding the panel mid-commit is therefore
|
||||
/// safe, and `panel_hidden` is not consulted by placement at all.
|
||||
/// `params.side` is likewise unreachable — `set_params` refuses it,
|
||||
/// and only `apply_placement`'s created branch ever writes it, so a
|
||||
/// body cannot turn an already-dedicated document window into the
|
||||
/// side slot.
|
||||
///
|
||||
/// # What is deliberately NOT refused
|
||||
///
|
||||
/// * **The document profile is untouched.** Its preflight already
|
||||
/// checked the same destination, and constraining its body would
|
||||
/// newly refuse dired's own documented panel path.
|
||||
/// * **Dedicating a *document* window is fine.** It cannot change
|
||||
/// which of panel-or-document a side request resolves to.
|
||||
/// * **Falling back is still allowed.** A frontend that cannot render
|
||||
/// a panel degrades gracefully exactly as it does today; this
|
||||
/// refuses the *mutation that manufactures* a fallback, never the
|
||||
/// fallback itself.
|
||||
pub(crate) fn panel_commit_dedication_refusal(&self, fid: FrontendId) -> Option<String> {
|
||||
let contract = self.commit_contract.as_ref()?;
|
||||
if contract.profile != CommitProfile::Panel {
|
||||
if contract.profile != CommitProfile::Panel || contract.destination.frontend != fid {
|
||||
return None;
|
||||
}
|
||||
let reason = self.document_destination_refusal(&contract.destination)?;
|
||||
Some(format!(
|
||||
"display: this \"panel\" commit fell back to a document window, and {reason}"
|
||||
))
|
||||
Some(
|
||||
"cannot dedicate the side window inside a \"panel\" commit_to --- the commit's \
|
||||
preflight was relaxed because this frontend places side requests in the panel, \
|
||||
and dedicating the one slot would silently redirect the result into a document \
|
||||
window instead (dedicate outside the commit, or use the \"document\" profile)"
|
||||
.to_string(),
|
||||
)
|
||||
}
|
||||
|
||||
/// Q#BP3's precedence: exact target, then side affinity, then
|
||||
|
|
|
|||
|
|
@ -908,6 +908,24 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
|||
None => None,
|
||||
};
|
||||
let dedicated = opts.get::<Option<bool>>("dedicated")?;
|
||||
// Q#DC-2 (revision 8). The direct route to the one
|
||||
// mutation that could make a `"panel"` commit's
|
||||
// relaxed preflight wrong. Refused BEFORE the borrow
|
||||
// below, so the attempt changes nothing --- including
|
||||
// `fixed_rows`, which is in the same option table.
|
||||
if dedicated == Some(true) {
|
||||
let core = cc.borrow();
|
||||
if core
|
||||
.windows
|
||||
.get(&id)
|
||||
.is_some_and(crate::window::Window::is_side)
|
||||
&& let Some(reason) = core.panel_commit_dedication_refusal(fid)
|
||||
{
|
||||
return Err(mlua::Error::runtime(format!(
|
||||
"pmacs.window.set_params: {reason}"
|
||||
)));
|
||||
}
|
||||
}
|
||||
{
|
||||
let mut core = cc.borrow_mut();
|
||||
let window = core.windows.get_mut(&id).ok_or_else(|| {
|
||||
|
|
|
|||
|
|
@ -20,17 +20,20 @@
|
|||
//! * **A refusal is asserted on its reason**, never on the mere fact
|
||||
//! that something failed. `commit_to` has five distinct refusals and a
|
||||
//! raise; "it errored" would pass on any of the wrong ones.
|
||||
//! * **The panel profile's relaxation is pinned at BOTH of its
|
||||
//! evaluation sites** (revision 7). The preflight is an early refusal
|
||||
//! that spares the body; the guarantee is enforced where placement
|
||||
//! resolves, because the body is arbitrary synchronous Lua and can
|
||||
//! create the fallback *after* any snapshot was taken — refusing
|
||||
//! `await` stops a second coroutine interleaving, not the body's own
|
||||
//! statements. Three tests carry that split and none subsumes another:
|
||||
//! * **The panel profile's relaxation is pinned as a preflight PLUS the
|
||||
//! refusal that keeps it true** (revision 8). The preflight measures
|
||||
//! whether this frontend places side requests in the panel; the body is
|
||||
//! arbitrary *synchronous* Lua, so refusing `await` — which only stops
|
||||
//! another coroutine interleaving — does not stop it invalidating that
|
||||
//! measurement. The answer is neither to predict the body nor to catch
|
||||
//! it late at placement (by then it has created buffers, handles and
|
||||
//! paint, which is "four mutations too late" all over again) but to
|
||||
//! **refuse the mutation at the attempt**, exactly as `await` is
|
||||
//! refused. Three tests carry it and none subsumes another:
|
||||
//! `a_panel_commit_that_falls_back_runs_the_document_preflight` (the
|
||||
//! body must not run),
|
||||
//! `a_panel_commit_whose_body_creates_the_fallback_is_refused_at_placement`
|
||||
//! (the result must not land), and
|
||||
//! body must not run at all when the fallback already holds),
|
||||
//! `a_body_that_tries_to_create_the_fallback_is_refused_at_the_attempt`
|
||||
//! (the mutation is refused, and nothing partial is left behind), and
|
||||
//! `a_panel_commit_that_falls_back_with_a_valid_destination_still_lands`
|
||||
//! (falling back is still graceful degradation, not an error).
|
||||
//!
|
||||
|
|
@ -90,6 +93,32 @@ fn name_in(s: &EditorState, window: WindowId) -> String {
|
|||
registry.get(buffer).expect("buffer").name().to_string()
|
||||
}
|
||||
|
||||
/// Whether `window` is pinned to its buffer (Q#BP2c `dedicated`).
|
||||
fn dedicated(s: &EditorState, window: WindowId) -> bool {
|
||||
s.core
|
||||
.borrow()
|
||||
.windows
|
||||
.get(&window)
|
||||
.is_some_and(|w| w.params.dedicated)
|
||||
}
|
||||
|
||||
/// Whether a buffer by this name exists at all.
|
||||
///
|
||||
/// The "nothing partial was installed" assertion needs to see a side
|
||||
/// effect the body would have left *before* reaching any display, and a
|
||||
/// created-but-never-shown buffer is exactly that.
|
||||
fn buffer_exists(s: &EditorState, name: &str) -> bool {
|
||||
eval(
|
||||
s,
|
||||
&format!(
|
||||
"for _, id in ipairs(pmacs.buffer.list()) do
|
||||
if pmacs.describe.buffer(id).name == {name:?} then return true end
|
||||
end
|
||||
return false"
|
||||
),
|
||||
)
|
||||
}
|
||||
|
||||
fn local_window(s: &EditorState) -> WindowId {
|
||||
s.core
|
||||
.borrow()
|
||||
|
|
@ -454,6 +483,13 @@ fn the_preflight_matrix_holds_in_both_profiles() {
|
|||
const PANEL_BODY: &str = "pmacs.window.display(pmacs.buffer.create('*result*'), \
|
||||
{ side = 'bottom' })";
|
||||
|
||||
/// A reusable panel: present and **undedicated**, so the preflight
|
||||
/// measures "this frontend places side requests in the panel" and the
|
||||
/// relaxation applies. Every mutation row starts from here except the
|
||||
/// one whose whole point is that no panel exists yet.
|
||||
const PANEL_ARRANGED: &str = "pmacs.window.display(pmacs.buffer.create('*pinned*'), \
|
||||
{ side = 'bottom', dedicated = false, select = false })";
|
||||
|
||||
/// Arrange one of the two reasons a side request falls back into a
|
||||
/// document window, and assert the arrangement took.
|
||||
///
|
||||
|
|
@ -578,95 +614,185 @@ fn a_panel_commit_that_falls_back_runs_the_document_preflight() {
|
|||
}
|
||||
}
|
||||
|
||||
/// **N** — the case no preflight snapshot can catch: the **body itself**
|
||||
/// creates the fallback, and the refusal still fires.
|
||||
/// **N** — a body that tries to **create** the fallback is refused **at
|
||||
/// the attempt**, and the refusal lands on the mutation rather than on
|
||||
/// the outcome.
|
||||
///
|
||||
/// This is why the guarantee moved to the placement boundary. Revision 6
|
||||
/// argued that a prediction taken at preflight could not go stale,
|
||||
/// because `commit_to`'s body cannot `await`. Refusing `await` prevents
|
||||
/// another *coroutine* interleaving; it places no restriction on the body
|
||||
/// itself, which is arbitrary Lua running synchronously:
|
||||
/// This is the case no preflight snapshot can catch, and the two rows
|
||||
/// above cannot reach it: both establish their fallback state *before*
|
||||
/// `commit_to` is entered. The body is arbitrary **synchronous** Lua, so
|
||||
/// refusing `await` — which stops another coroutine interleaving —
|
||||
/// places no restriction on it:
|
||||
///
|
||||
/// ```lua
|
||||
/// pmacs.window.set_params(pmacs.window.panel(), { dedicated = true })
|
||||
/// pmacs.window.display(result, { side = "bottom" })
|
||||
/// ```
|
||||
///
|
||||
/// Two statements. The first invalidates the prediction, the second cashes
|
||||
/// it in. The arrangement here is deliberately the **inverse** of the
|
||||
/// preflight rows: an undedicated panel exists, so the prediction says
|
||||
/// "this will land in the panel", the relaxation applies, and the body
|
||||
/// runs. Only when placement resolves is the fallback a fact.
|
||||
/// Two statements: the first invalidates the preflight, the second cashes
|
||||
/// it in. The arrangement is deliberately the **inverse** of the rows
|
||||
/// above — the preflight says "this lands in the panel", the relaxation
|
||||
/// applies, and the body runs.
|
||||
///
|
||||
/// What it asserts, and why each is load-bearing:
|
||||
/// **Asserting only "document B was not replaced" is insufficient**, and
|
||||
/// an earlier version of this test made exactly that mistake: it passes
|
||||
/// on a design that lets the body mutate freely and merely declines the
|
||||
/// final installation, leaving every other side effect behind. So the
|
||||
/// three assertions that matter are that the **dedication call itself is
|
||||
/// refused**, the slot is **still undedicated afterwards**, and **nothing
|
||||
/// partial was installed**.
|
||||
///
|
||||
/// * the body **did** run — otherwise the test would be re-proving the
|
||||
/// preflight and this whole case would be untested;
|
||||
/// * the refusal arrives as a **raise** from `display`, since the body was
|
||||
/// already running and there is no `(false, reason)` left to return —
|
||||
/// asserted on content, and it names both the fallback and the
|
||||
/// stale-intent reason;
|
||||
/// * `*newer*` is **still in the document window**. That is the actual
|
||||
/// user-visible guarantee; everything above it is mechanism.
|
||||
/// # One row per WRITE SITE, not per call spelling
|
||||
///
|
||||
/// *Mutation:* delete the `fallback_commit_refusal` call from
|
||||
/// `display_buffer`. This test fails on all three; every other test in
|
||||
/// this file still passes, which is precisely the hole revision 6 left.
|
||||
/// A single row is exactly what would let a second route keep the
|
||||
/// defect — which is not hypothetical: review found the
|
||||
/// `display{side, dedicated}` route *after* `set_params` was specified.
|
||||
/// So the rows are chosen to hit each distinct write to
|
||||
/// `Window::params.dedicated` that a side window can receive, rather
|
||||
/// than each way of phrasing the call:
|
||||
///
|
||||
/// | row | reaches |
|
||||
/// |---|---|
|
||||
/// | `set_params` | the direct write in the binding (Q#BP2c) |
|
||||
/// | `display{side, dedicated}` replacing | `apply_placement`'s **replacing** arm |
|
||||
/// | `display{side, dedicated}` same buffer | its **non-replacing** arm |
|
||||
/// | `display{side, dedicated}` with no panel | its **created** arm |
|
||||
///
|
||||
/// The three `display` rows converge on one guard, in `display_buffer` —
|
||||
/// `apply_placement` has exactly one caller, so every request-driven
|
||||
/// dedication passes through it. They are still separate rows because
|
||||
/// that convergence is a property of today's call graph, and a row per
|
||||
/// arm fails loudly if it stops holding.
|
||||
///
|
||||
/// The rest of the enumeration is **unreachable rather than refused**
|
||||
/// and is recorded in `EditorCore::panel_commit_dedication_refusal`,
|
||||
/// because a test cannot express it: `panel_capable` has no Lua binding;
|
||||
/// **losing** the side window is not a fallback route at all
|
||||
/// (`resolve_placement` creates a fresh panel instead); and `quit`
|
||||
/// restoring a `dedicated: true` presentation cannot be constructed,
|
||||
/// since `QuitAction::Restore` only captures that flag on a *replacing*
|
||||
/// side placement and a dedicated slot can never be the target of one.
|
||||
///
|
||||
/// *Mutation:* delete the `panel_commit_dedication_refusal` call from
|
||||
/// either guarded site — `set_params` drops row 1, `display_buffer`
|
||||
/// drops rows 2–4 — and every other test in this file still passes.
|
||||
#[test]
|
||||
fn a_panel_commit_whose_body_creates_the_fallback_is_refused_at_placement() {
|
||||
let s = editor();
|
||||
|
||||
// A REUSABLE panel: undedicated, so the preflight prediction says
|
||||
// this frontend places side requests in the panel.
|
||||
exec(
|
||||
&s,
|
||||
"pmacs.window.display(pmacs.buffer.create('*pinned*'),
|
||||
{ side = 'bottom', dedicated = false, select = false })",
|
||||
);
|
||||
capture(&s);
|
||||
let doc = local_window(&s);
|
||||
exec(
|
||||
&s,
|
||||
"pmacs.window.switch_buffer(pmacs.buffer.create('*newer*'))",
|
||||
);
|
||||
assert_eq!(
|
||||
name_in(&s, doc),
|
||||
"*newer*",
|
||||
"the arrangement must make the captured window stale"
|
||||
);
|
||||
|
||||
commit_body(
|
||||
&s,
|
||||
Some("'panel'"),
|
||||
&format!(
|
||||
"pmacs.window.set_params(pmacs.window.panel(), {{ dedicated = true }})
|
||||
{PANEL_BODY}"
|
||||
fn a_body_that_tries_to_create_the_fallback_is_refused_at_the_attempt() {
|
||||
// (label, panel arrangement before the capture, attempted mutation)
|
||||
let routes: [(&str, &str, &str); 4] = [
|
||||
(
|
||||
"set_params",
|
||||
PANEL_ARRANGED,
|
||||
"pmacs.window.set_params(pmacs.window.panel(), { dedicated = true })",
|
||||
),
|
||||
);
|
||||
(
|
||||
"display{side, dedicated} replacing",
|
||||
PANEL_ARRANGED,
|
||||
"pmacs.window.display(pmacs.buffer.create('*usurp*'),
|
||||
{ side = 'bottom', dedicated = true, select = false })",
|
||||
),
|
||||
(
|
||||
// The same buffer the panel already shows: `replacing` is
|
||||
// false, so this lands in a DIFFERENT arm of the same
|
||||
// function, which a row against the replacing arm alone
|
||||
// would not exercise.
|
||||
"display{side, dedicated} same buffer",
|
||||
PANEL_ARRANGED,
|
||||
"pmacs.window.display(pmacs.window.buffer(pmacs.window.panel()),
|
||||
{ side = 'bottom', dedicated = true, select = false })",
|
||||
),
|
||||
(
|
||||
// NO panel at capture time: the preflight relaxes because
|
||||
// `side_window_for` is None (a side request would CREATE a
|
||||
// panel, never fall back). The body then creates one
|
||||
// dedicated, which makes the next side request fall back.
|
||||
"display{side, dedicated} creating the panel",
|
||||
"",
|
||||
"pmacs.window.display(pmacs.buffer.create('*usurp*'),
|
||||
{ side = 'bottom', dedicated = true, select = false })",
|
||||
),
|
||||
];
|
||||
|
||||
assert!(
|
||||
ran(&s),
|
||||
"the body must have run -- the preflight could not have known, and a test where \
|
||||
it did not run would be re-proving the preflight"
|
||||
);
|
||||
let raised = raised(&s).expect(
|
||||
"the refusal arrives as a raise: the body was already running, so there is no \
|
||||
(false, reason) return left to make",
|
||||
);
|
||||
assert!(
|
||||
raised.contains("fell back to a document window"),
|
||||
"the message must name what happened; got {raised:?}"
|
||||
);
|
||||
assert!(
|
||||
raised.contains("now shows another buffer"),
|
||||
"and which document precondition failed; got {raised:?}"
|
||||
);
|
||||
assert_eq!(
|
||||
name_in(&s, doc),
|
||||
"*newer*",
|
||||
"the user's newer buffer must survive -- this is the guarantee, and it is what a \
|
||||
preflight-only design cannot provide"
|
||||
);
|
||||
for (label, arrange, attempt) in routes {
|
||||
let s = editor();
|
||||
exec(&s, arrange);
|
||||
|
||||
let panel_before = s.core.borrow().side_window_for(FrontendId::LOCAL);
|
||||
if let Some(panel) = panel_before {
|
||||
assert!(
|
||||
!dedicated(&s, panel),
|
||||
"{label}: the slot must start UNDEDICATED, or the preflight would have \
|
||||
refused and this row would be re-proving the preflight"
|
||||
);
|
||||
}
|
||||
let panel_buffer_before = panel_before.map(|panel| name_in(&s, panel));
|
||||
|
||||
capture(&s);
|
||||
let doc = local_window(&s);
|
||||
exec(
|
||||
&s,
|
||||
"pmacs.window.switch_buffer(pmacs.buffer.create('*newer*'))",
|
||||
);
|
||||
|
||||
commit_body(&s, Some("'panel'"), &format!("{attempt}\n{PANEL_BODY}"));
|
||||
|
||||
assert!(
|
||||
ran(&s),
|
||||
"{label}: the body must have run -- the preflight could not have known"
|
||||
);
|
||||
|
||||
// 1. THE MUTATION ITSELF IS REFUSED, on content.
|
||||
let raised = raised(&s).unwrap_or_else(|| {
|
||||
panic!("{label}: the attempted mutation must be refused, not merely declined later")
|
||||
});
|
||||
assert!(
|
||||
raised.contains("cannot dedicate the side window"),
|
||||
"{label}: the refusal must name the operation it is refusing; got {raised:?}"
|
||||
);
|
||||
assert!(
|
||||
raised.contains("\"panel\" commit_to"),
|
||||
"{label}: and why it is refused here specifically; got {raised:?}"
|
||||
);
|
||||
|
||||
// 2. THE SLOT IS STILL UNDEDICATED -- including the row where
|
||||
// the slot would have been created dedicated, which must
|
||||
// leave no slot at all rather than an undedicated one.
|
||||
let panel_after = s.core.borrow().side_window_for(FrontendId::LOCAL);
|
||||
assert_eq!(
|
||||
panel_after, panel_before,
|
||||
"{label}: a refused mutation must not have created or removed the side slot"
|
||||
);
|
||||
if let Some(panel) = panel_after {
|
||||
assert!(
|
||||
!dedicated(&s, panel),
|
||||
"{label}: a refused mutation must not have happened -- the whole design \
|
||||
rests on the preflight's measurement still being true afterwards"
|
||||
);
|
||||
}
|
||||
|
||||
// 3. NOTHING PARTIAL WAS INSTALLED.
|
||||
if let (Some(panel), Some(before)) = (panel_after, panel_buffer_before.as_ref()) {
|
||||
assert_eq!(
|
||||
&name_in(&s, panel),
|
||||
before,
|
||||
"{label}: the panel must still show what it showed"
|
||||
);
|
||||
}
|
||||
assert_eq!(
|
||||
name_in(&s, doc),
|
||||
"*newer*",
|
||||
"{label}: and the user's newer buffer must survive"
|
||||
);
|
||||
assert!(
|
||||
!buffer_exists(&s, "*result*"),
|
||||
"{label}: the refusal must land BEFORE the body's own display -- a `*result*` \
|
||||
buffer means the commit got partway and then stopped"
|
||||
);
|
||||
assert!(
|
||||
!buffer_exists(&s, "*usurp*") || panel_after == panel_before,
|
||||
"{label}: no usurping presentation may have been installed"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// **P** — a `"panel"` commit that falls back with a **still-valid**
|
||||
|
|
|
|||
Loading…
Reference in New Issue