Skip to content

explorer: document loadRes-chase invariant on tryEnterPointModeIfNeeded (closes #194) #195

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rdhyee merged 2 commits into from
May 10, 2026
Merged

explorer: document loadRes-chase invariant on tryEnterPointModeIfNeeded (closes #194) #195

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9abfa89
explorer: document loadRes-chase invariant on tryEnterPointModeIfNeed…
rdhyee May 10, 2026
b87cb49
explorer: tighten loadRes-chase invariant doc per Codex review
rdhyee May 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions explorer.qmd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1628,11 +1628,27 @@ zoomWatcher = {
// long) `loadRes` await for the same reason: if the user zooms back out
// or another path enters point mode during the wait, we must not force
// entry afterwards.
//
// INVARIANT: every `loadRes` call site in this cell *outside this
// helper* that could be in flight when the user crosses below
// `ENTER_POINT_ALT` MUST be followed by `await tryEnterPointModeIfNeeded()`.
// The `!loading` short-circuit below relies on this — when an unrelated
// `loadRes` is in flight we bail and leave recovery to that call site's
// own post-await chase. A new `loadRes` caller added without the chase
// would silently break supersession recovery and only surface as a rare
// liveness regression (see issue #194). Verify with:
// grep -nE "await[[:space:]]+loadRes\(" explorer.qmd
// which lists exactly the awaited call sites (one inside this helper,
// and one per external caller). For each external match, confirm it is
// immediately followed by `await tryEnterPointModeIfNeeded()`.
async function tryEnterPointModeIfNeeded() {
if (mode === 'point') return;
if (viewer.camera.positionCartographic.height >= ENTER_POINT_ALT) return;

let res8Ready = currentRes === 8;
// See INVARIANT above: if an unrelated load is in flight, that
// call site is responsible for chasing with this helper when it
// settles. Don't second-guess it from here.
if (!res8Ready && !loading) {
res8Ready = await loadRes(8, h3_res8_url, {
loadingMsg: 'Fetching sample index…',
Expand Down
Loading