Navigate recorded History positions with a measured REPL rail (#881, 3/3) (#887)

* 🚧 Give navigation its own snapshot, and measure the rail — layers 1 and 3a

**Layer 1.** `ReplHistoryNavigation` is the one reading taken at the whole
file rather than at the selected prefix: a marker and a kind per retained
position, and the head. No label, no source, no name, no value, no outcome
detail — a reader standing at an earlier position learns *that* later
positions exist and what kind they are, and nothing about what they hold.

Both halves now come from one acknowledged array. `reproject` snapshots it,
projects the whole file for the summary and the requested prefix for every
other pane, and drops the full model rather than keeping it, so nothing
downstream can reach a later entry through it. A later malformed segment
refuses the whole reading, including for an earlier marker.

The head is derived on read, not cached: pausing, resuming and the last of an
entry's resources releasing all change it while the file stands still. Its
liveness fact is PR 2's entry-wide signal, which stays true until the outer
Agent attachment and the consumers have gone — a body that returned and a root
Close that was recorded are both earlier than that.

**Layer 3a.** `history-rail.ts` prepares the five rows from engine
measurements. The right-hand caption column is reserved once for *every* head
label, so a head change re-cuts nothing; the rail is what remains; marks are
placed at `round(i × (W−1)/(K−1))` and a lone position goes where the head is.
Collisions become one visual group that keeps every member, and each category
colours itself from its own members — a group holding a passed entry and an
unreached minor position is both, and one colour would lose half of it.

Two defects the tests found. The caption merge loop read its bound from the
list it was shrinking, so it stopped before the last pair joined. And the
band's minimum is its title plus the reserved head column — 49 columns — which
three of my own cases were below; they were asking for a refusal and reading
it as a bug.

`repl-history.test.ts`: 16 steps, every width from a real engine.

* 🚧 Draw the band as a measured rail, and give the drawer the whole order

The band was a list of checkpoint labels wrapped across five rows. It is now
the rail the handoff froze: a title and the head on row 1, entry captions and
the selection caption on row 2, tall uprisers on 3, the rule on 4, minor stems
and the head's marker on 5. Marks are placed from engine measurements, the
right-hand caption column is reserved once for every head label, and layout
receives inert text and roles — no Journal, no session, no capability.

The History drawer now reads navigation rather than the selected prefix, and
says what each position *is* — `12 · Agent turn recorded` — counted from the
thin list rather than looked up, because looking it up would mean reading a
payload the summary deliberately does not carry.

One real defect, caught by the too-small profile: the band was being prepared
for a frame that publishes no footer, turning a refusal the product already
handles into a measurement failure.

The replaced premises, itemized. Nine assertions across five suites, each with
the claim it still makes:

  - `repl-terminal`'s label-grouping case is **retired**, not re-anchored: it
    asserted that a compact band shares labels and that each marker names the
    others sharing one, and the band has no labels. Its surviving claim — a
    compact band never costs a reader an exact position — is now
    `repl-history`'s "keeps every member", made against the real engine at two
    widths and checking ordinals as well as markers. It is not re-anchored in
    place because that suite drives a fixture surface that carries an empty
    band, so the case would have asserted grouping that nothing grouped.
  - `UI5` keeps placement and full-width rows and drops reading a label out of
    the band; `G1` asserted one accent for the whole band and now asserts that
    every cell is one of the band's own roles.
  - `UI15` had two premises this slice reverses: a drawer row holds no `·`
    (they all carry their ordinal now) and a frozen prefix lists fewer
    positions than the head (it lists the whole order — that *is* the
    navigation exception).
  - `repl-agent-journey`'s J3 asserted that an earlier prefix offers no later
    marker. It does now; what it must not do is show what that marker holds,
    and the pair is asserted together.
  - `focusedOn` steps past a row's ordinal, as it already stepped past the
    focus and selection cues.

Frozen commands: 93 tests / 301 steps and 19 / 111, both exit 0; whitespace
gate on the endpoint diff exits 0.

* 🚧 Prove the head against a real session — layer 2's evidence

H3 drives `openReplSession` rather than calling the derivation: empty before
an entry exists, live from before its first record, settled once its outcome
is retained and nothing of it is still standing.

The case that matters is SETTLING. An installation of the entry's own reads
the head at the moment it is released — after the root closed and before the
entry's work had finished — and finds `settling`. A head taken from the root
Close alone would have called that finished, which is the defect the frozen
precedence exists to prevent.

And the summary carries no payload: a `<Json>` holding `shibboleth` leaves
nothing of it in the navigation, whose points have exactly `marker` and
`kind`.

* 📝 Say what the band shows and what the head means

`specs/repl-spec.md` gains the five rows, the measured reservation, the
proportional placement, grouping that keeps every position selectable, and the
seven head readings with their precedence. `architecture.md` gains the two new
modules and the navigation exception: one acknowledged array per wake, two
projections of it, the full model discarded from child reachability, and a
head that changes while the file stands still so it rides the existing wake.

Both in present tense, and both say the thing that is easy to lose: the band
is the one reading not taken at the selected prefix, and that exception is for
the band and not for capabilities.

* ✅ Prove navigation is the whole order while content is one prefix (#881)

* ✅ Reach every recorded position, and open an early prefix cold (#881)

* ✨ Read navigation and content from one snapshot, and prove the rest (#881)

* 🚨 Sort through a copy, so the Node typecheck accepts the History proofs (#881)

`tsconfig.node.json` pins `lib` to ES2022 and `toSorted` is ES2023, so the
three `toSorted` calls in the History suite failed `tsc` in every `test-node`
shard before a single test ran — ten identical shard failures, and the `green`
gate with them. `deno check`, `deno task test` and `pnpm lint` all passed,
and oxlint's `no-array-sort` actively recommends `toSorted`, so nothing local
said otherwise.

Sort a copy instead, which keeps what `toSorted` was chosen for: `ordinals`
arrives `readonly`, and nothing observes the order of the array sorted here.
`Object.keys` already returns a fresh array, so that one sorts in place.

The three remaining `no-array-sort` warnings are the lib's cost, and the
comment at the first site says so.

Author: taras

architecture.md

@@ -5745,6 +5745,8 @@ DurableEvents -> frozen ReplModel -> resolved immutable view
 | `description.ts` | opaque immutable descriptions and the closed action boundary |
 | `reconcile.ts` | reconciling descriptions into one mounted Freedom tree |
 | `handoff.ts` | the acknowledged commit boundary |
+| `navigation.ts` | every retained position and the head, as the one reading taken at the whole file |
+| `history-rail.ts` | the five-row History band, placed from engine measurements |
 | `source-reading.ts` | one entry as output and then source, with what each element is doing |
 | `presentation-text.ts` · `presentation-style.ts` | what the characters of a reading are, and the colours it is drawn in |
 | `fitting.ts` | engine-measured widths, and the rows a reading is cut into |
@@ -5756,6 +5758,46 @@ DurableEvents -> frozen ReplModel -> resolved immutable view
 | `components/` · `application.ts` | the screens, and the one state transition boundary |
 | `storage.ts` · `program.ts` | where histories live, and the command as one scope |
 
+### Navigation is the whole file; content is one prefix
+
+Every pane reads the selected prefix. The History band and its drawer are the
+explicit exception, and the only one: they read a thin summary of the *whole*
+validated file — a marker and a kind per retained position, plus the head —
+because the positions after the selected one are where a reader can go next.
+No label, source, name, value, outcome detail or observation is in it, so
+nothing a later position holds reaches a reading of an earlier one.
+
+Both halves come from one acknowledged event array per wake: the full file for
+the summary, the requested marker for everything else, through the projector's
+existing whole-file validation. The full model is discarded from child
+reachability rather than kept, so nothing downstream can walk to a later entry
+through it, and navigation is never assembled by appending to a selected
+model. A later malformed segment refuses the whole reading even for an earlier
+marker — the alternative is stale navigation standing beside a prefix that
+still looks plausible.
+
+The session hands both halves over together, as one reading, and the root
+carries that one value through resolution, paint and resize rather than asking
+again for either half. It has to: the root reads the terminal's size between
+resolving a frame and composing it, that read suspends, and a record can be
+retained while it does. Content taken before it and navigation taken after it
+would describe two different files on one screen. A resize recomposes the
+reading that was resolved at a new size, never at a new snapshot.
+
+When that reading cannot be built at all — a record this process wrote and can
+no longer read — the root draws the refused view, the same screen a cold open
+of the same file shows. That is a different outcome from a route that does not
+resolve at its position: there, a reading still stands and the reason is said
+beside it. A refusal has nothing to stand beside, so nothing is left on the
+screen pretending to be current.
+
+The head is derived on read from retained facts and from work this session
+owns, never from a body's return, a recorded root Close, a component badge or
+the selected content. It changes while the file stands still, so it publishes
+through the wake the session and the controller already send; History adds no
+stream, timer or clock. The inspected action row keeps its historical
+restrictions: navigation is the exception for the band, not for capabilities.
+
 ### Sequential entries over one physical journal
 
 One execution is one append-only stream, and entries are ranges of it. A segment

packages/cli/src/repl/application.ts

@@ -47,8 +47,6 @@ import {
   drawerLayerProps,
   drawerRect,
   footerProps,
-  historyBand,
-  HISTORY_ROWS,
   inspectionWidth,
   paneColumnProps,
   paneContentProps,
@@ -82,6 +80,10 @@ import type { ReplAdmission, ReplWindow } from "./layout-admission.ts";
 import { ORDINARY, REPL_PALETTE, styleOf } from "./presentation-style.ts";
 import type { ReplPresentationRole, ReplRowStyle } from "./presentation-style.ts";
 import { jsonRuns, sourceRuns } from "./presentation-text.ts";
+import { NO_NAVIGATION, numbered, pointLabel } from "./navigation.ts";
+import type { ReplHistoryNavigation } from "./navigation.ts";
+import { blankBand, EMPTY_BAND, HISTORY_ROWS } from "./history-rail.ts";
+import type { ReplPreparedRail } from "./history-rail.ts";
 import { entryReading, NO_READING } from "./source-reading.ts";
 import type { ReplReading } from "./source-reading.ts";
 import { readingRuns } from "./fitting.ts";
@@ -532,6 +534,16 @@ export interface ReplTransition {
 export interface ReplView {
   readonly state: ReplState;
   readonly model: ReplModel;
+  /**
+   * Every position the history retained, and what the head is doing.
+   *
+   * The explicit exception to this view being a reading of one prefix: the
+   * band is a map of the whole recorded order, because the positions after
+   * the selected one are where a reader can go next. It is a marker and a
+   * kind each — nothing a later position holds crosses — and it reaches the
+   * band and the History drawer only. Every other pane gets the prefix.
+   */
+  readonly navigation: ReplHistoryNavigation;
   readonly selection: ReplSelection;
   readonly live: ReplLive;
   /** The canonical location this view is at. */
@@ -758,6 +770,7 @@ export function viewFor(
   live: ReplLive,
   size: ReplTerminalSize,
   focused?: string,
+  navigation: ReplHistoryNavigation = NO_NAVIGATION,
 ): Result<ReplView> {
   // This process is the only thing that can say a question is waiting, so it
   // says so here rather than leaving resolution to infer it from a history that
@@ -790,6 +803,7 @@ export function viewFor(
     Object.freeze({
       state,
       model,
+      navigation,
       selection: resolved.value,
       live: shown,
       location: encodeLocation(state.route),
@@ -812,6 +826,9 @@ export function refusedView(
   return Object.freeze({
     state,
     model: EMPTY_MODEL,
+    // A refusal navigates nowhere: there is no validated reading to draw a
+    // rail from, and a stale one beside a refusal would be the worst of both.
+    navigation: NO_NAVIGATION,
     selection: Object.freeze({
       route: state.route,
       surface: state.route.surface,
@@ -2790,6 +2807,20 @@ export function readingOf(view: ReplView): ReplReading {
   });
 }
 
+/**
+ * The band's five rows, or five empty ones where none was prepared.
+ *
+ * The measuring pass has no rail — it is the pass that answers how wide the
+ * band is — and an unmeasured frame describes no band content, exactly as it
+ * describes no windowed content.
+ */
+function bandRowsOf(
+  rail: ReplPreparedRail | undefined,
+  columns: number,
+): readonly (readonly ReplTokenRun[])[] {
+  return rail === undefined ? blankBand(columns) : rail.rows;
+}
+
 /**
  * The transcript rows the selected locus holds.
  *
@@ -3383,14 +3414,20 @@ function drawerContent(
     // not described, so it is not a cell, not a target and not a Tab stop —
     // which is what makes reaching the last one a thing the controls do rather
     // than something clipping hides.
-    for (const checkpoint of view.model.checkpoints) {
+    // The whole recorded order, not the selected prefix: the positions after
+    // the one being read are where a reader can go next, and a drawer that
+    // stopped at the selection would be a list of where they had already
+    // been. Every position gets its own row — a group is how the rail *draws*
+    // two of them, never how it counts them — and each says what kind it is
+    // without reading anything the position holds.
+    for (const one of numbered(view.navigation)) {
       content.push({
         described: row(
-          `drawer:marker:${checkpoint.marker}`,
-          padControl(checkpoint.label, width),
-          { select: "marker", marker: checkpoint.marker },
+          `drawer:marker:${one.point.marker}`,
+          padControl(pointLabel(one.point, one.ordinal, one.entry), width),
+          { select: "marker", marker: one.point.marker },
           styleOf("history", {
-            selected: view.state.route.at === checkpoint.marker,
+            selected: view.state.route.at === one.point.marker,
             inspected: true,
           }),
           { here: view.focused },
@@ -4126,6 +4163,14 @@ export interface ReplPresentationContext {
    * prepared rows; it cannot recover the rest of an unprepared one.
    */
   readonly preview: readonly ReplFittedLine[] | undefined;
+  /**
+   * The History band this frame measured, or none before it has measured one.
+   *
+   * Prepared beside the reading: where a mark lands is a proportion of the
+   * rail's measured columns, so the pass that asks how wide the band is
+   * cannot already have placed anything on it.
+   */
+  readonly rail: ReplPreparedRail | undefined;
 }
 
 /** One reading's descriptions, paired with where the engine places them. */
@@ -4451,13 +4496,10 @@ export function presentationFor(
   }
   const size = view.size;
   const profile = profileFor(size);
-  const band = historyBand(
-    view.model.checkpoints.map((checkpoint) => ({
-      marker: checkpoint.marker,
-      label: checkpoint.label,
-    })),
-    size.columns,
-  );
+  // The band the frame measured. The pass that asks how wide it is has none,
+  // and describes none: a rail placed against a width still being asked for
+  // would be a rail placed on nothing.
+  const rail = context.rail;
   if (profile === "too-small") {
     // No cell beyond the sentence, so nothing this frame hides can be pointed
     // at: a control that is not in the frame is not in its target map either.
@@ -4487,7 +4529,7 @@ export function presentationFor(
         actions: undefined,
         regions: Object.freeze([Object.freeze({ region: "refusal", id: "box:refusal" })]),
         contents: Object.freeze([]),
-        history: band,
+        history: rail ?? EMPTY_BAND,
       }),
     };
   }
@@ -4790,14 +4832,16 @@ export function presentationFor(
                 id: "box:footer:band",
                 region: "footer",
                 props: bandProps(),
-                children: band.rows.map((text, at) =>
+                children: bandRowsOf(rail, size.columns).map((row, at) =>
                   box({
                     id: `box:band:${at}`,
                     region: "footer",
                     props: rowProps(size.columns),
-                    text,
+                    text: runText(row),
+                    runs: row,
                     // The one part of this screen that is not a mounted row, so
                     // its style comes from the band rather than from a candidate.
+                    // Each cell carries its own role; this is the row's base.
                     style: styleOf("history", {
                       inspected: view.state.route.at !== undefined,
                     }),
@@ -4822,7 +4866,7 @@ export function presentationFor(
       }),
       regions: Object.freeze(regions.map((region) => Object.freeze(region))),
       contents: Object.freeze(contents.map((content) => Object.freeze(content))),
-      history: band,
+      history: rail ?? EMPTY_BAND,
     }),
   };
 }