feat(window): a destination any async continuation can capture
Journey Stage 1a built `pmacs.window.commit_to` for the continuation boundary --- "the listing settles a tick or more later, and by then the ambient frontend, selected window, and active buffer may all name something else" --- but nothing outside the `path.open-directory` dispatch could mint a destination to hand it. Every other async Lua continuation therefore resolved its target from ambient state a tick after the request, which is PR #227's P1a finding: run `git.status` in frontend A, let B become active, and A's panel opens in B. This is the prerequisite lane #227 blocks on (`docs/destination-capture-framing.md`, revision 5). No adopter here: git's adoption is #227's work, since a prerequisite that converts its own first consumer cannot be reviewed separately from it. Three parts. **`pmacs.window.capture_destination()`** returns the same nonconstructible userdata for the current frontend. No arguments, and that is load-bearing rather than minimal (Q#DC-1): a Lua-supplied frontend id would reintroduce exactly the fabrication hole the userdata design closes. Profile-blind for the same kind of reason (Q#DC-4) --- capture freezes what is true now, and what a commit depends on is declared later, at the commit. **`DirectoryDestination` -> `ViewDestination`**, with the Lua userdata and the capture renamed to match. The captured triple was already generic; only its name and its capture site were not. The document pair is now `Option`, set and cleared together, so a frontend with no live document window still captures rather than returning nothing and sending the caller back to the ambient state this exists to replace. **`commit_to(dest, body [, profile])`** (Q#DC-2/Q#DC-5), a closed set of two. The document profile keeps all four preflight checks. The panel profile keeps only the first --- the requesting frontend still has a layout --- because a panel result does not occupy the captured document window, does not replace its buffer, and does not need it to exist, so each of the other three would refuse for a reason unrelated to what the continuation does. Omitting the profile means `"document"`, which is what makes the preservation promise contractual rather than careful: every existing two-argument caller keeps all four checks by definition of the signature. The profile argument is typed `mlua::Value`, NOT `Option<String>`, so its error is REACHABLE: with the narrower type mlua rejects a number or a table during argument conversion, before the closure body runs, and the message naming the accepted values never appears. That is the same trap the `dest` argument documents one position to its left. `nil` and absence are the same answer; anything else is refused by one message that names both accepted values. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
a177d61bf3
commit
9fee5618ee
|
|
@ -1801,7 +1801,7 @@ fn open_initial_target(
|
||||||
let (buffer_id, fire) = match resolved {
|
let (buffer_id, fire) = match resolved {
|
||||||
crate::editor_core::ResolvedTarget::Directory { path } => {
|
crate::editor_core::ResolvedTarget::Directory { path } => {
|
||||||
let dest = editor
|
let dest = editor
|
||||||
.capture_directory_destination(frontend_id, origin_window)
|
.capture_view_destination(frontend_id, origin_window)
|
||||||
.ok_or_else(|| format!("cannot open {}: no document window", path.display()))?;
|
.ok_or_else(|| format!("cannot open {}: no document window", path.display()))?;
|
||||||
editor.dispatch_directory_open(&path, dest);
|
editor.dispatch_directory_open(&path, dest);
|
||||||
editor.reconcile_panel_layout(frontend_id);
|
editor.reconcile_panel_layout(frontend_id);
|
||||||
|
|
|
||||||
|
|
@ -1219,22 +1219,32 @@ impl EditorState {
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Capture the destination a directory open must commit to
|
/// Capture the destination a directory open must commit to
|
||||||
/// (Q#JR14), or `None` when `frontend` has no document window.
|
/// (Q#JR14), or `None` when `window` is gone.
|
||||||
///
|
///
|
||||||
/// Synchronous by necessity: the listing settles a tick or more
|
/// Synchronous by necessity: the listing settles a tick or more
|
||||||
/// later, and by then the ambient frontend, selected window, and
|
/// later, and by then the ambient frontend, selected window, and
|
||||||
/// active buffer may all name something else.
|
/// active buffer may all name something else.
|
||||||
pub(crate) fn capture_directory_destination(
|
///
|
||||||
|
/// Takes the window **explicitly**, unlike
|
||||||
|
/// [`crate::editor_core::EditorCore::capture_view_destination`],
|
||||||
|
/// which reads the ambient one. Both directory callers already hold
|
||||||
|
/// the exact window the open was resolved against — the daemon's is
|
||||||
|
/// read before `resolve_target_buffer` runs (Q#BP11b) — and
|
||||||
|
/// recapturing it from ambient state here would discard that.
|
||||||
|
/// A directory open therefore always yields a full document pair,
|
||||||
|
/// which is why this keeps returning `Option` rather than the total
|
||||||
|
/// capture's `ViewDestination`.
|
||||||
|
pub(crate) fn capture_view_destination(
|
||||||
&self,
|
&self,
|
||||||
frontend: crate::protocol::FrontendId,
|
frontend: crate::protocol::FrontendId,
|
||||||
window: crate::window::WindowId,
|
window: crate::window::WindowId,
|
||||||
) -> Option<crate::editor_core::DirectoryDestination> {
|
) -> Option<crate::editor_core::ViewDestination> {
|
||||||
let core = self.core.borrow();
|
let core = self.core.borrow();
|
||||||
let buffer = core.windows.get(&window)?.buffer_id;
|
let buffer = core.windows.get(&window)?.buffer_id;
|
||||||
Some(crate::editor_core::DirectoryDestination {
|
Some(crate::editor_core::ViewDestination {
|
||||||
frontend,
|
frontend,
|
||||||
window,
|
window: Some(window),
|
||||||
buffer,
|
buffer: Some(buffer),
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1258,7 +1268,7 @@ impl EditorState {
|
||||||
.borrow()
|
.borrow()
|
||||||
.primary_document_window(crate::protocol::FrontendId::LOCAL);
|
.primary_document_window(crate::protocol::FrontendId::LOCAL);
|
||||||
let dest = window.and_then(|window| {
|
let dest = window.and_then(|window| {
|
||||||
self.capture_directory_destination(crate::protocol::FrontendId::LOCAL, window)
|
self.capture_view_destination(crate::protocol::FrontendId::LOCAL, window)
|
||||||
});
|
});
|
||||||
let Some(dest) = dest else {
|
let Some(dest) = dest else {
|
||||||
self.core.borrow_mut().status =
|
self.core.borrow_mut().status =
|
||||||
|
|
@ -1288,13 +1298,13 @@ impl EditorState {
|
||||||
pub(crate) fn dispatch_directory_open(
|
pub(crate) fn dispatch_directory_open(
|
||||||
&mut self,
|
&mut self,
|
||||||
path: &std::path::Path,
|
path: &std::path::Path,
|
||||||
dest: crate::editor_core::DirectoryDestination,
|
dest: crate::editor_core::ViewDestination,
|
||||||
) {
|
) {
|
||||||
let display = path.display().to_string();
|
let display = path.display().to_string();
|
||||||
let args = {
|
let args = {
|
||||||
let lua = self.lua_host.lua();
|
let lua = self.lua_host.lua();
|
||||||
let destination =
|
let destination =
|
||||||
match lua.create_userdata(crate::lua_bindings::DirectoryDestinationLua(dest)) {
|
match lua.create_userdata(crate::lua_bindings::ViewDestinationLua(dest)) {
|
||||||
Ok(userdata) => mlua::Value::UserData(userdata),
|
Ok(userdata) => mlua::Value::UserData(userdata),
|
||||||
Err(error) => {
|
Err(error) => {
|
||||||
self.core.borrow_mut().status = format!("cannot open {display}: {error}");
|
self.core.borrow_mut().status = format!("cannot open {display}: {error}");
|
||||||
|
|
|
||||||
|
|
@ -130,39 +130,55 @@ pub enum ResolvedTarget {
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Where a directory open was requested, captured **synchronously** at
|
/// Where an asynchronous continuation's result belongs, captured
|
||||||
/// resolve time (Journey Stage 1a, Q#JR14).
|
/// **synchronously** at request time (Journey Stage 1a, Q#JR14;
|
||||||
|
/// generalized by `docs/destination-capture-framing.md`).
|
||||||
///
|
///
|
||||||
/// The listing that satisfies a directory open is asynchronous
|
/// The work that satisfies such a request is asynchronous (a directory
|
||||||
/// (`pmacs.fs.read_dir` is worker-dispatched and must be awaited), so the
|
/// listing is worker-dispatched and must be awaited; so is a `git`
|
||||||
/// code that finally builds and displays the listing runs a tick or more
|
/// invocation), so the code that finally builds and displays the result
|
||||||
/// later — outside interactive dispatch, where `pmacs.window.*` acts on
|
/// runs a tick or more later — outside interactive dispatch, where
|
||||||
/// the *ambient* frontend by documented design (`builtin/runtime/dired.lua`).
|
/// `pmacs.window.*` acts on the *ambient* frontend by documented design
|
||||||
/// Without a captured destination, a second frontend dispatching in the
|
/// (`builtin/runtime/dired.lua`). Without a captured destination, a
|
||||||
/// meantime silently redirects the listing.
|
/// second frontend dispatching in the meantime silently redirects the
|
||||||
|
/// result.
|
||||||
///
|
///
|
||||||
/// All three fields are load-bearing:
|
/// 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:
|
||||||
///
|
///
|
||||||
/// * `frontend` — the scope the commit must run in.
|
/// * `frontend` — the scope the commit must run in. Always present.
|
||||||
/// * `window` — the exact destination; the ambient selected window is
|
/// * `window` — the exact destination; the ambient selected window is
|
||||||
/// not it.
|
/// not it. Absent when the frontend had no document window at capture
|
||||||
|
/// time.
|
||||||
/// * `buffer` — what that window held at capture time, so **stale
|
/// * `buffer` — what that window held at capture time, so **stale
|
||||||
/// intent loses to the user** (Q#JR14c). A user who replaced the
|
/// intent loses to the user** (Q#JR14c). A user who replaced the
|
||||||
/// buffer while the listing was in flight is newer information than
|
/// buffer while the work was in flight is newer information than the
|
||||||
/// the launch argument, and must not be overwritten.
|
/// launch argument, and must not be overwritten. Present exactly when
|
||||||
|
/// `window` is.
|
||||||
|
///
|
||||||
|
/// The pair is set or cleared together — see
|
||||||
|
/// [`EditorCore::capture_view_destination`], which is the only place
|
||||||
|
/// that reads them off ambient state.
|
||||||
|
///
|
||||||
|
/// Which of those a commit actually requires is the **profile**, chosen
|
||||||
|
/// at `pmacs.window.commit_to` rather than at capture (Q#DC-2/Q#DC-5):
|
||||||
|
/// the document profile requires all of them, the panel profile requires
|
||||||
|
/// only a live `frontend`. Capture stays profile-blind so a caller does
|
||||||
|
/// not have to know at capture time what it will do at commit time.
|
||||||
///
|
///
|
||||||
/// Exposed to Lua only as nonconstructible userdata (Q#JR14d): as a
|
/// Exposed to Lua only as nonconstructible userdata (Q#JR14d): as a
|
||||||
/// table, the *same* value is handed to every resolver listener in turn,
|
/// table, the *same* value is handed to every resolver listener in turn,
|
||||||
/// so one could mutate it and then decline — redirecting later listeners
|
/// so one could mutate it and then decline — redirecting later listeners
|
||||||
/// — and any Lua could fabricate a plausible triple.
|
/// — and any Lua could fabricate a plausible triple.
|
||||||
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
|
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
|
||||||
pub struct DirectoryDestination {
|
pub struct ViewDestination {
|
||||||
/// Frontend that requested the directory.
|
/// Frontend that requested the work.
|
||||||
pub frontend: FrontendId,
|
pub frontend: FrontendId,
|
||||||
/// Window the listing must land in.
|
/// Window the result must land in, when there is one.
|
||||||
pub window: WindowId,
|
pub window: Option<WindowId>,
|
||||||
/// Buffer that window held at capture time (stale-intent check).
|
/// Buffer that window held at capture time (stale-intent check).
|
||||||
pub buffer: BufferId,
|
pub buffer: Option<BufferId>,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// A `display_buffer` request (Q#BP3).
|
/// A `display_buffer` request (Q#BP3).
|
||||||
|
|
@ -3042,6 +3058,33 @@ impl EditorCore {
|
||||||
self.non_side_target(fid).ok()
|
self.non_side_target(fid).ok()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Capture where `fid`'s next asynchronous result belongs (Q#JR14,
|
||||||
|
/// generalized by Q#DC-1/Q#DC-4).
|
||||||
|
///
|
||||||
|
/// **Profile-blind and total**: it records what is there rather than
|
||||||
|
/// what a caller intends to do later, and it never fails while a
|
||||||
|
/// frontend id exists. A frontend with no document window yields a
|
||||||
|
/// destination carrying only `frontend` — enough for a panel commit,
|
||||||
|
/// and refused by a document commit with a reason naming the missing
|
||||||
|
/// window. Returning `None` here instead would push the caller back
|
||||||
|
/// onto ambient state, which is the misrouting the capture exists to
|
||||||
|
/// remove.
|
||||||
|
///
|
||||||
|
/// 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.
|
||||||
|
#[must_use]
|
||||||
|
pub fn capture_view_destination(&self, fid: FrontendId) -> ViewDestination {
|
||||||
|
let pair = self
|
||||||
|
.primary_document_window(fid)
|
||||||
|
.and_then(|window| Some((window, self.windows.get(&window)?.buffer_id)));
|
||||||
|
ViewDestination {
|
||||||
|
frontend: fid,
|
||||||
|
window: pair.map(|(window, _)| window),
|
||||||
|
buffer: pair.map(|(_, buffer)| buffer),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/// [`Self::primary_document_window`]'s buffer, falling back to the
|
/// [`Self::primary_document_window`]'s buffer, falling back to the
|
||||||
/// focused window's when the layout is degenerate.
|
/// focused window's when the layout is degenerate.
|
||||||
#[must_use]
|
#[must_use]
|
||||||
|
|
|
||||||
|
|
@ -4239,25 +4239,34 @@ fn install_path_module(lua: &Lua) -> mlua::Result<Table> {
|
||||||
Ok(path)
|
Ok(path)
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Lua handle for a captured directory destination (Q#JR14d).
|
/// Lua handle for a captured view destination (Q#JR14d).
|
||||||
///
|
///
|
||||||
/// Deliberately **nonconstructible from Lua** and read-only. The same
|
/// Deliberately **nonconstructible from Lua** and read-only, which the
|
||||||
/// value is passed to every `path.open-directory` listener in turn: as a
|
/// generalization to `pmacs.window.capture_destination()` preserves:
|
||||||
/// table, an earlier listener could mutate it and then decline,
|
/// capture mints one from editor state, and there is still no
|
||||||
/// redirecting later listeners or the fallback to a window the user
|
/// constructor and no setter. The same value is passed to every
|
||||||
/// never asked for — and any Lua could fabricate a plausible
|
/// `path.open-directory` listener in turn: as a table, an earlier
|
||||||
/// frontend/window/buffer triple and hand it to `commit_to`. Userdata
|
/// listener could mutate it and then decline, redirecting later
|
||||||
/// with no constructor and no setters makes both unrepresentable rather
|
/// listeners or the fallback to a window the user never asked for — and
|
||||||
/// than merely discouraged.
|
/// any Lua could fabricate a plausible frontend/window/buffer triple and
|
||||||
|
/// hand it to `commit_to`. Userdata with no constructor and no setters
|
||||||
|
/// makes both unrepresentable rather than merely discouraged.
|
||||||
///
|
///
|
||||||
/// The single accessor exists because dired needs the exact window for
|
/// The single accessor exists because dired needs the exact window for
|
||||||
/// its `display{window = …}` target; nothing needs the frontend or the
|
/// its `display{window = …}` target; nothing needs the frontend or the
|
||||||
/// captured buffer, which stay private to the preflight.
|
/// captured buffer, which stay private to the preflight.
|
||||||
pub(crate) struct DirectoryDestinationLua(pub(crate) crate::editor_core::DirectoryDestination);
|
///
|
||||||
|
/// `window()` returns **nil** when the capturing frontend had no
|
||||||
|
/// document window (Q#DC-4) — such a destination is still commitable
|
||||||
|
/// under the panel profile, so the accessor reports the absence rather
|
||||||
|
/// than inventing an id.
|
||||||
|
pub(crate) struct ViewDestinationLua(pub(crate) crate::editor_core::ViewDestination);
|
||||||
|
|
||||||
impl mlua::UserData for DirectoryDestinationLua {
|
impl mlua::UserData for ViewDestinationLua {
|
||||||
fn add_methods<M: mlua::UserDataMethods<Self>>(methods: &mut M) {
|
fn add_methods<M: mlua::UserDataMethods<Self>>(methods: &mut M) {
|
||||||
methods.add_method("window", |_, this, ()| Ok(this.0.window.raw()));
|
methods.add_method("window", |_, this, ()| {
|
||||||
|
Ok(this.0.window.map(crate::window::WindowId::raw))
|
||||||
|
});
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -63,6 +63,65 @@ pub(crate) fn acting_frontend(lua: &Lua, core: &SharedCore) -> FrontendId {
|
||||||
.unwrap_or_else(|| core.borrow().active_frontend_key())
|
.unwrap_or_else(|| core.borrow().active_frontend_key())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Which of `commit_to`'s preconditions a body actually depends on
|
||||||
|
/// (Q#DC-2).
|
||||||
|
///
|
||||||
|
/// A **closed** set of two, not an open string namespace: a third
|
||||||
|
/// profile is a decision about what a continuation may depend on, not a
|
||||||
|
/// spelling. Chosen at `commit_to` rather than at capture, because the
|
||||||
|
/// caller knows what it is about to do only then.
|
||||||
|
#[derive(Clone, Copy, PartialEq, Eq)]
|
||||||
|
enum CommitProfile {
|
||||||
|
/// The body replaces the captured window's buffer: **all four**
|
||||||
|
/// preflight checks apply. This is what an omitted profile means,
|
||||||
|
/// so every caller written before the profile existed keeps exactly
|
||||||
|
/// the guarantees it was written against.
|
||||||
|
Document,
|
||||||
|
/// The body puts its result somewhere that is not the captured
|
||||||
|
/// document window — a bottom panel, typically. Only the "requesting
|
||||||
|
/// frontend still has a layout" check applies; see the preflight for
|
||||||
|
/// why each of the other three is *deliberately* omitted.
|
||||||
|
Panel,
|
||||||
|
}
|
||||||
|
|
||||||
|
/// One message for every bad profile — an unrecognized string and a
|
||||||
|
/// non-string alike (Q#DC-5).
|
||||||
|
///
|
||||||
|
/// Stated once so the parser and the message cannot drift, and phrased
|
||||||
|
/// to name the accepted values *and* the default, because a caller who
|
||||||
|
/// gets this wrong is guessing at the vocabulary.
|
||||||
|
const BAD_COMMIT_PROFILE: &str = "pmacs.window.commit_to: profile must be the string \"document\" \
|
||||||
|
or \"panel\" (omitting it, or passing nil, means \"document\")";
|
||||||
|
|
||||||
|
/// Resolve the optional third argument of `commit_to`.
|
||||||
|
///
|
||||||
|
/// Takes a [`Value`] rather than an `Option<String>` **so this refusal
|
||||||
|
/// is reachable**: with the narrower type mlua rejects a number or a
|
||||||
|
/// table during argument conversion, before the closure body runs, and
|
||||||
|
/// the caller gets a generic conversion error that names neither the
|
||||||
|
/// accepted values nor the default. That is the same trap the `dest`
|
||||||
|
/// argument documents at its own borrow site.
|
||||||
|
///
|
||||||
|
/// `Nil` and absence are the **same** answer, not two: a Lua caller
|
||||||
|
/// threading an optional variable produces `commit_to(dest, body, nil)`,
|
||||||
|
/// and a third behaviour there would stay invisible until someone hit
|
||||||
|
/// it.
|
||||||
|
fn commit_profile(value: &Value) -> mlua::Result<CommitProfile> {
|
||||||
|
match value {
|
||||||
|
Value::Nil => Ok(CommitProfile::Document),
|
||||||
|
Value::String(name) => match &*name.to_str()? {
|
||||||
|
"document" => Ok(CommitProfile::Document),
|
||||||
|
"panel" => Ok(CommitProfile::Panel),
|
||||||
|
// An unrecognized profile ERRORS rather than falling back to
|
||||||
|
// the document one: a fallback would silently hand a caller
|
||||||
|
// stricter or looser checks than it asked for, which is the
|
||||||
|
// failure the parameterization exists to prevent.
|
||||||
|
_ => Err(mlua::Error::runtime(BAD_COMMIT_PROFILE)),
|
||||||
|
},
|
||||||
|
_ => Err(mlua::Error::runtime(BAD_COMMIT_PROFILE)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/// Run the panel-reconciliation transaction from a Lua-owning context
|
/// Run the panel-reconciliation transaction from a Lua-owning context
|
||||||
/// (Q#BP2b).
|
/// (Q#BP2b).
|
||||||
///
|
///
|
||||||
|
|
@ -452,7 +511,7 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
||||||
"commit_to",
|
"commit_to",
|
||||||
lua.create_function(
|
lua.create_function(
|
||||||
move |lua,
|
move |lua,
|
||||||
(dest, body): (mlua::Value, mlua::Function)|
|
(dest, body, profile): (mlua::Value, mlua::Function, mlua::Value)|
|
||||||
-> mlua::Result<mlua::MultiValue> {
|
-> mlua::Result<mlua::MultiValue> {
|
||||||
// Journey Stage 1a (Q#JR14). Preflight FIRST, then
|
// Journey Stage 1a (Q#JR14). Preflight FIRST, then
|
||||||
// scope, then run. The ordering is the whole point:
|
// scope, then run. The ordering is the whole point:
|
||||||
|
|
@ -472,7 +531,7 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
||||||
// rule nor how to get a real destination.
|
// rule nor how to get a real destination.
|
||||||
let dest = match &dest {
|
let dest = match &dest {
|
||||||
mlua::Value::UserData(userdata) => {
|
mlua::Value::UserData(userdata) => {
|
||||||
userdata.borrow::<super::DirectoryDestinationLua>().ok()
|
userdata.borrow::<super::ViewDestinationLua>().ok()
|
||||||
}
|
}
|
||||||
_ => None,
|
_ => None,
|
||||||
};
|
};
|
||||||
|
|
@ -484,43 +543,74 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
||||||
)
|
)
|
||||||
})?
|
})?
|
||||||
.0;
|
.0;
|
||||||
|
// Q#DC-5. Resolved AFTER the destination so a caller
|
||||||
|
// who got both wrong hears about the destination
|
||||||
|
// first --- it is the argument that cannot be fixed
|
||||||
|
// by reading this signature.
|
||||||
|
let profile = commit_profile(&profile)?;
|
||||||
|
|
||||||
// 1. The requesting frontend still has a layout.
|
|
||||||
let refusal = {
|
let refusal = {
|
||||||
let core = cc.borrow();
|
let core = cc.borrow();
|
||||||
|
// 1. The requesting frontend still has a layout.
|
||||||
|
// Required by BOTH profiles: it is the whole
|
||||||
|
// of the panel profile (Q#DC-2), because a
|
||||||
|
// frontend that is gone can host nothing.
|
||||||
if !core.views.contains_key(&dest.frontend) {
|
if !core.views.contains_key(&dest.frontend) {
|
||||||
Some("requesting frontend is gone".to_string())
|
Some("requesting frontend is gone".to_string())
|
||||||
} else if !core
|
} else if profile == CommitProfile::Panel {
|
||||||
.views
|
// 2, 3 and 4 are DELIBERATELY OMITTED here,
|
||||||
.get(&dest.frontend)
|
// not overlooked (Q#DC-2). A panel result
|
||||||
.is_some_and(|view| view.layout.iter_ids().contains(&dest.window))
|
// does not occupy the captured document
|
||||||
{
|
// window, does not replace its buffer, and
|
||||||
// 2. The destination window is still live in it.
|
// does not need it to exist --- so each of
|
||||||
Some(format!("window {} is gone", dest.window.raw()))
|
// those checks would refuse for a reason
|
||||||
} else if core
|
// unrelated to what the continuation does,
|
||||||
.windows
|
// and a refusal a user cannot explain is how
|
||||||
.get(&dest.window)
|
// a mechanism gets worked around. Every one
|
||||||
.is_some_and(|w| w.buffer_id != dest.buffer)
|
// of the three is pinned as NOT refusing
|
||||||
{
|
// under this profile.
|
||||||
// 3. Stale intent (Q#JR14c): the user
|
|
||||||
// replaced the buffer while the work was
|
|
||||||
// in flight. Their action is newer
|
|
||||||
// information than the request, so the
|
|
||||||
// request loses.
|
|
||||||
Some(format!(
|
|
||||||
"window {} now shows another buffer",
|
|
||||||
dest.window.raw()
|
|
||||||
))
|
|
||||||
} else if !core.window_accepts_buffer(dest.window, None) {
|
|
||||||
// 4. Replaceability (Q#JR14f). `None`
|
|
||||||
// because the replacement does not exist
|
|
||||||
// yet — passing the captured buffer would
|
|
||||||
// approve a window dedicated to *it*, and
|
|
||||||
// the handler's different buffer would be
|
|
||||||
// refused later, after mutating.
|
|
||||||
Some(format!("window {} is dedicated", dest.window.raw()))
|
|
||||||
} else {
|
|
||||||
None
|
None
|
||||||
|
} else if let Some(window) = dest.window {
|
||||||
|
if !core
|
||||||
|
.views
|
||||||
|
.get(&dest.frontend)
|
||||||
|
.is_some_and(|view| view.layout.iter_ids().contains(&window))
|
||||||
|
{
|
||||||
|
// 2. The destination window is still live in it.
|
||||||
|
Some(format!("window {} is gone", window.raw()))
|
||||||
|
} else if core
|
||||||
|
.windows
|
||||||
|
.get(&window)
|
||||||
|
.is_some_and(|w| Some(w.buffer_id) != dest.buffer)
|
||||||
|
{
|
||||||
|
// 3. Stale intent (Q#JR14c): the user
|
||||||
|
// replaced the buffer while the work was
|
||||||
|
// in flight. Their action is newer
|
||||||
|
// information than the request, so the
|
||||||
|
// request loses.
|
||||||
|
Some(format!("window {} now shows another buffer", window.raw()))
|
||||||
|
} else if !core.window_accepts_buffer(window, None) {
|
||||||
|
// 4. Replaceability (Q#JR14f). `None`
|
||||||
|
// because the replacement does not exist
|
||||||
|
// yet — passing the captured buffer would
|
||||||
|
// approve a window dedicated to *it*, and
|
||||||
|
// the handler's different buffer would be
|
||||||
|
// refused later, after mutating.
|
||||||
|
Some(format!("window {} is dedicated", window.raw()))
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
// The capture found no document window
|
||||||
|
// (Q#DC-4). A refusal rather than a raise, so
|
||||||
|
// it joins the four above as one more thing
|
||||||
|
// the destination can fail to satisfy and an
|
||||||
|
// adopter handles it the same way.
|
||||||
|
Some(
|
||||||
|
"destination has no document window (capture it from a frontend \
|
||||||
|
that has one, or commit with the \"panel\" profile)"
|
||||||
|
.to_string(),
|
||||||
|
)
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
if let Some(reason) = refusal {
|
if let Some(reason) = refusal {
|
||||||
|
|
@ -563,6 +653,39 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
|
||||||
)?;
|
)?;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
{
|
||||||
|
// Q#DC-1 — the capture half, reachable from Lua at last.
|
||||||
|
//
|
||||||
|
// Journey Stage 1a built `commit_to` for the continuation
|
||||||
|
// boundary, but the only thing that could mint a destination was
|
||||||
|
// the `path.open-directory` dispatch, so every other async
|
||||||
|
// continuation had to resolve its target from ambient state a
|
||||||
|
// tick after the request --- which is a misrouting waiting for a
|
||||||
|
// second frontend to become active.
|
||||||
|
//
|
||||||
|
// NO ARGUMENTS, and that is load-bearing rather than
|
||||||
|
// minimalism. A Lua-supplied frontend id would reintroduce
|
||||||
|
// exactly the fabrication hole the nonconstructible userdata
|
||||||
|
// closes (Q#JR14d): the point of userdata is that Lua names a
|
||||||
|
// destination it was *given*, never one it composed.
|
||||||
|
//
|
||||||
|
// PROFILE-BLIND, likewise (Q#DC-4). Capture records what is
|
||||||
|
// there; what a commit depends on is declared at `commit_to`,
|
||||||
|
// because a caller knows what it is about to do only then.
|
||||||
|
// Making capture profile-aware would force it to know at capture
|
||||||
|
// time what it will do at commit time, which is the opposite of
|
||||||
|
// why capture exists --- freeze the truth early, decide later.
|
||||||
|
let cc = core.clone();
|
||||||
|
win.set(
|
||||||
|
"capture_destination",
|
||||||
|
lua.create_function(move |lua, ()| {
|
||||||
|
let fid = acting_frontend(lua, &cc);
|
||||||
|
let dest = cc.borrow().capture_view_destination(fid);
|
||||||
|
lua.create_userdata(super::ViewDestinationLua(dest))
|
||||||
|
})?,
|
||||||
|
)?;
|
||||||
|
}
|
||||||
|
|
||||||
{
|
{
|
||||||
// Q#S3-1 — the shared adopter-display rule, reachable from Lua.
|
// Q#S3-1 — the shared adopter-display rule, reachable from Lua.
|
||||||
//
|
//
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue