feat(gpu): 1-pre --- the redraw family, which sends the daemon nothing
The second of the two arms with no outbound traffic. `RedrawRequested` joins the lifecycle family and its body moves to `App::apply_redraw`. This is the arm P2 was written for. With `CloseRequested` it makes the pair a harness built on protocol traffic could not see at all: neither one sends the daemon a byte, so "did this arm get handled?" has no answer in a transcript of daemon traffic. The transcript row now drives five events of which two are silent. The lifecycle family's criterion is stated properly here rather than left as the accident of which three arms happened to be smallest: events about the WINDOW ITSELF --- closing, resizing, repainting --- as against a gesture aimed into the document. `ModifiersChanged` is the one exception and is documented as one, since it is a bare state mutation with no gesture of its own and no body to extract. Evidence --- 7 rows, 2 further mutations: M7 `RedrawRequested` -> no family -> the redraw row (+ transcript) M8 harness records outbound only -> the transcript row ALONE M8 is M4 re-run now that a second silent arm exists: the mutation discards both `Exit` and `Redraw` and keeps only the resize, and still fails exactly one row, because the per-variant rows assert `feed`'s return value and the transcript row alone owns P2. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
014110fb90
commit
7f0f9db98c
|
|
@ -2703,6 +2703,14 @@ impl App {
|
||||||
// daemon can act on changed.
|
// daemon can act on changed.
|
||||||
self.flush_panel_geometry(GeometryTrigger::Surface);
|
self.flush_panel_geometry(GeometryTrigger::Surface);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Perform [`LifecycleRoute::Redraw`]. A no-op before `resumed` has
|
||||||
|
/// built the surface.
|
||||||
|
fn apply_redraw(&mut self) {
|
||||||
|
if let Some(state) = self.state.as_mut() {
|
||||||
|
state.render();
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// GUI Stage 1-pre — the input seam.
|
/// GUI Stage 1-pre — the input seam.
|
||||||
|
|
@ -2720,11 +2728,11 @@ impl App {
|
||||||
///
|
///
|
||||||
/// The decision is what the route *is*, not merely which family claims
|
/// The decision is what the route *is*, not merely which family claims
|
||||||
/// it: `Exit` is the local exit effect, `Resize` carries the clamped
|
/// it: `Exit` is the local exit effect, `Resize` carries the clamped
|
||||||
/// surface extent, `Modifiers` carries the state mutation. Two arms
|
/// surface extent, `Modifiers` carries the state mutation. **Two arms —
|
||||||
/// (`CloseRequested`, and `RedrawRequested` once it moves here) send
|
/// `CloseRequested` and `RedrawRequested` — send nothing outbound at
|
||||||
/// nothing outbound at all, so a harness recording only protocol traffic
|
/// all**, so a harness recording only protocol traffic would leave them
|
||||||
/// would leave them invisible — which is why a route names its local
|
/// invisible; that is why a route names its local effect and the harness
|
||||||
/// effect and the harness records routes.
|
/// records routes.
|
||||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||||
enum Route {
|
enum Route {
|
||||||
/// The lifecycle family — see [`route_lifecycle`].
|
/// The lifecycle family — see [`route_lifecycle`].
|
||||||
|
|
@ -2736,9 +2744,11 @@ enum Route {
|
||||||
Unrouted,
|
Unrouted,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// The lifecycle family: the three arms that read no pointer state, hold
|
/// The lifecycle family: events about the **window itself** — closing,
|
||||||
/// no `State` borrow, and reach the socket only through the resize
|
/// resizing, repainting — rather than about a gesture aimed into the
|
||||||
/// declaration.
|
/// document. `ModifiersChanged` is grouped here as the one exception,
|
||||||
|
/// and it is named as one: it is a bare state mutation with no gesture
|
||||||
|
/// of its own and no body to extract.
|
||||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||||
enum LifecycleRoute {
|
enum LifecycleRoute {
|
||||||
/// `CloseRequested` — leave the event loop. Q#S1-1: a native close
|
/// `CloseRequested` — leave the event loop. Q#S1-1: a native close
|
||||||
|
|
@ -2753,6 +2763,10 @@ enum LifecycleRoute {
|
||||||
/// defensive padding; deciding it here is what makes it witnessable
|
/// defensive padding; deciding it here is what makes it witnessable
|
||||||
/// without a surface.
|
/// without a surface.
|
||||||
Resize { width: u32, height: u32 },
|
Resize { width: u32, height: u32 },
|
||||||
|
/// `RedrawRequested` — paint a frame. Nothing goes to the daemon,
|
||||||
|
/// which is why the harness records local effects rather than
|
||||||
|
/// outbound traffic.
|
||||||
|
Redraw,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Decide what `window_event` should do with an event, from the event
|
/// Decide what `window_event` should do with an event, from the event
|
||||||
|
|
@ -2774,6 +2788,7 @@ fn route_lifecycle(event: &WindowEvent) -> Option<LifecycleRoute> {
|
||||||
width: size.width.max(1),
|
width: size.width.max(1),
|
||||||
height: size.height.max(1),
|
height: size.height.max(1),
|
||||||
}),
|
}),
|
||||||
|
WindowEvent::RedrawRequested => Some(LifecycleRoute::Redraw),
|
||||||
_ => None,
|
_ => None,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -2897,6 +2912,18 @@ mod input_routing_tests {
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// P1 — `RedrawRequested`. The second arm that sends the daemon
|
||||||
|
/// nothing, and the reason the harness cannot be a transcript of
|
||||||
|
/// outbound traffic.
|
||||||
|
#[test]
|
||||||
|
fn redraw_requested_routes_to_redraw() {
|
||||||
|
let mut harness = RoutingHarness::default();
|
||||||
|
assert_eq!(
|
||||||
|
harness.feed(&WindowEvent::RedrawRequested),
|
||||||
|
Route::Lifecycle(LifecycleRoute::Redraw)
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
/// An event no family claims. `Occluded` is chosen because pmacs has
|
/// An event no family claims. `Occluded` is chosen because pmacs has
|
||||||
/// never handled it and no later slice will — a still-inline family
|
/// never handled it and no later slice will — a still-inline family
|
||||||
/// would also read `Unrouted` today and stop doing so when it moves.
|
/// would also read `Unrouted` today and stop doing so when it moves.
|
||||||
|
|
@ -2907,14 +2934,16 @@ mod input_routing_tests {
|
||||||
}
|
}
|
||||||
|
|
||||||
/// P2 — the harness records a transcript, and the transcript
|
/// P2 — the harness records a transcript, and the transcript
|
||||||
/// distinguishes the three lifecycle effects from each other and
|
/// distinguishes each lifecycle effect from the others and from an
|
||||||
/// from an unclaimed event. Two of these four rows produce no
|
/// unclaimed event. **Two of these five rows produce no outbound
|
||||||
/// outbound traffic whatsoever.
|
/// traffic whatsoever**, which is the property that rules out a
|
||||||
|
/// harness built on protocol traffic alone.
|
||||||
#[test]
|
#[test]
|
||||||
fn the_harness_records_each_local_effect_in_order() {
|
fn the_harness_records_each_local_effect_in_order() {
|
||||||
let mut harness = RoutingHarness::default();
|
let mut harness = RoutingHarness::default();
|
||||||
harness.feed(&WindowEvent::Resized(PhysicalSize::new(800, 600)));
|
harness.feed(&WindowEvent::Resized(PhysicalSize::new(800, 600)));
|
||||||
harness.feed(&modifiers_changed(ModifiersState::SHIFT));
|
harness.feed(&modifiers_changed(ModifiersState::SHIFT));
|
||||||
|
harness.feed(&WindowEvent::RedrawRequested);
|
||||||
harness.feed(&WindowEvent::Occluded(false));
|
harness.feed(&WindowEvent::Occluded(false));
|
||||||
harness.feed(&WindowEvent::CloseRequested);
|
harness.feed(&WindowEvent::CloseRequested);
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
|
|
@ -2925,6 +2954,7 @@ mod input_routing_tests {
|
||||||
height: 600,
|
height: 600,
|
||||||
}),
|
}),
|
||||||
Route::Lifecycle(LifecycleRoute::Modifiers(ModifiersState::SHIFT)),
|
Route::Lifecycle(LifecycleRoute::Modifiers(ModifiersState::SHIFT)),
|
||||||
|
Route::Lifecycle(LifecycleRoute::Redraw),
|
||||||
Route::Unrouted,
|
Route::Unrouted,
|
||||||
Route::Lifecycle(LifecycleRoute::Exit),
|
Route::Lifecycle(LifecycleRoute::Exit),
|
||||||
]
|
]
|
||||||
|
|
@ -3606,11 +3636,6 @@ impl ApplicationHandler<AppEvent> for App {
|
||||||
eprintln!("pmacs-gpu: wheel send_viewport failed: {e}");
|
eprintln!("pmacs-gpu: wheel send_viewport failed: {e}");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
WindowEvent::RedrawRequested => {
|
|
||||||
if let Some(state) = self.state.as_mut() {
|
|
||||||
state.render();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
// Stage 1-pre — everything the router already claims. The
|
// Stage 1-pre — everything the router already claims. The
|
||||||
// arms above are the families not yet moved behind it; when
|
// arms above are the families not yet moved behind it; when
|
||||||
// the last one goes, this match collapses to the call below
|
// the last one goes, this match collapses to the call below
|
||||||
|
|
@ -3621,6 +3646,7 @@ impl ApplicationHandler<AppEvent> for App {
|
||||||
Route::Lifecycle(LifecycleRoute::Resize { width, height }) => {
|
Route::Lifecycle(LifecycleRoute::Resize { width, height }) => {
|
||||||
self.apply_resize(width, height);
|
self.apply_resize(width, height);
|
||||||
}
|
}
|
||||||
|
Route::Lifecycle(LifecycleRoute::Redraw) => self.apply_redraw(),
|
||||||
Route::Unrouted => {}
|
Route::Unrouted => {}
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue