Stacked proof animations — an accordion over pristine static lines

[ibenian]

Screen.Recording.2026-07-21.at.11.45.17.PM.mov

Try it

Stacked mode (the ☰ button, added in #498) turns a proof animation into an accordion: every step you've passed stays on screen as a dimmed history line, and each new step unfolds below the previous one — like a chalkboard that writes itself. This post is about the machinery that makes that work. For the term-morphing engine itself (the FLIP flights, ghosts, and phase sequencing that both modes share), see the earlier show & tell: #455 — none of that is repeated here.

Everything below lives in static/proof-animation/proof-animation.js and proof-animation.css.

The resting invariant: a column of pristine static lines

The whole design hangs on one invariant. Outside a transition, the stage holds a .pa-lines flex column with exactly one .pa-line per step in [0, current], each a fresh, untouched KaTeX render. No animation residue, no held transforms, no half-faded glyphs.

_syncLines(count) is the reconciler that restores this invariant, and it's deliberately cheap: it removes extra lines, appends missing ones, and re-renders a line only if its data-step doesn't match its position or a transition flagged it data-dirty. Untouched lines are left completely alone — stepping through a 12-line proof doesn't re-render 11 lines each time.

That one function does triple duty:

• Settle — after a successful transition, _syncLines(target + 1) replaces the animated DOM with pristine renders, dropping every leftover morph style in one move. (Same philosophy as single mode's "settle to a pristine final render", but here it's just reconciliation.)
• Self-healing — _stackedGoTo calls _syncLines(prev + 1) before animating. If a previous transition was interrupted mid-flight (user spams next, mode flips, tab hides), whatever mess it left is reconciled away before the new transition measures anything.
• Resting render — jumping to an arbitrary step, resizes, theme changes: all funnel through _renderStage() → _syncLines.

Interrupted transitions don't try to clean up after themselves at all. They just mark the lines they touched as dirty and bail on a token check; the next _syncLines re-renders exactly those lines and nothing else.

Advancing: open the space first, then fly into it

_stackedAdvance runs three phases, in an order chosen so nothing ever flies into a clipped or moving target:

1. Build the new lines. Lines for (prev, target] are appended. On a multi-step jump the intermediates render immediately and only fade in; the target line renders visibility: hidden — its glyphs get posed by the flight, so its final state never flashes before the morph reaches it.

2. Expand the accordion. The column animates its real height from old to new — not a transform. That's deliberate: the page and embed hosts watch the column with ResizeObservers, and a transform would let the animation grow visually while the layout reports the old size (embeds would clip the new line, then jump). In the same breath, the outgoing current line demotes: a WAAPI tween glides its font-size and opacity from full prominence down to the history style. The resting history look is pure CSS —

.pa-root { --pa-hist-scale: 0.8; --pa-hist-dim: 0.6; }
.pa-stacked .pa-line { font-size: calc(1em * var(--pa-hist-scale)); opacity: var(--pa-hist-dim); }
.pa-stacked .pa-line.pa-line-current { font-size: 1em; opacity: 1; }

— and the tween just reads those computed values as its keyframe targets, so the theme can retune the accordion without touching JS. Because history lines are smaller than the current one, the demote also makes room: the expansion and the shrink happen together, so the column grows less than a naive "add a full-size line" would.

3. The flight. Snapshot the (still static, untouched) previous line and run the standard morph into the hidden target line — the same _morphFlight single mode uses (see #455), with one twist: deleteGhosts: false. In single mode, terms that disappear between steps need ghost clones fading out mid-air. In stacked mode they don't — the disappearing terms are still right there, visible in the frozen line above. The history line is the delete ghost. A whole class of animation work just evaporates because the previous state never leaves the screen.

Top-anchoring matters here too (align-items: flex-start on the stage): earlier lines never move as the accordion grows below them, so mid-flight geometry stays valid.

Retreating: the target is never touched

Going backward is not the forward animation reversed, because of a second invariant: a resting history line is never mutated. The retreat has to land on a line that's already sitting there, pristine.

1. Promote first. The target line tweens back to full size/opacity before anything is measured, so the flight lands on its final full-size pose — not a shrunken one that then pops. The outgoing line pins its current size via inline overrides so the CSS class flip doesn't snap it mid-dissolve.
2. Clones fly home. Matched terms fly as clones lifted from the outgoing line, landing exactly on top of the identical glyphs already visible in the target line — then the clones are removed. The real target DOM never changes. One subtlety: a term whose id matched but whose glyph text changed doesn't fly (it would visibly land on a different symbol); it dissolves with the outgoing line instead.
3. Dissolve & collapse. Every abandoned line (target+1 … prev) fades out — each starting from its actual computed opacity, since the outgoing current line sits at 1 while intermediate history lines rest at the dim value. Then the column height tweens down (real height again, same ResizeObserver reasoning) and the settle removes the elements for good.

Fitting: one shared scale, width-only

Single mode scales one expression to fit a box. Stacked mode has N lines sharing one font scale, so _capOverflowStacked walks every visible line and shrinks the stage font just enough that the widest line fits. Height is never capped: report-style hosts simply grow with the column, and fixed-height hosts get .pa-lines-scroll — the column scrolls internally and _scrollToCurrent keeps the newest line in view after every transition.

Interactivity: only the current line is alive

Every line renders the same LaTeX pipeline, which means the same data-n term ids appear in multiple lines. Hover, tap-to-ask, and term highlights would be ambiguous across duplicates — so interactivity is scoped hard to the current line: _liveRoot() returns the .pa-line-current element in stacked mode, and the CSS only enables pointer affordances under .pa-line-current. History lines are inert by construction, not by event-handler bookkeeping.

Mode flips mid-flight

Stacked can be toggled while a transition is airborne. _setStacked issues a fresh interruption token before cancelling — the async transition runner survives its awaits, and without the token flip it would happily settle its lines into the rebuilt stage (a stacked column spilling into a single-mode stage, or vice versa). With it, every pending token check fails and the runner exits; the rebuild then renders the current step cleanly in the new mode. Hidden tabs take the same escape hatch: WAAPI clocks freeze when the page hides, so goTo snaps straight to the reconciled resting state instead of stalling mid-accordion.

---

The short version: stacked mode is a reconciler with an animation on the boundary. All state lives in one invariant (lines [0..current], pristine), one cheap function restores it from anywhere, and the accordion/flight work is free to be interrupted at any moment because nothing downstream ever trusts what it left behind.

Try it: open any proof and hit the ☰ button — e.g. the Tsiolkovsky rocket equation derivation at /renderproof?builtin=physics/tsiolkovsky-rocket-equation.

🤖 Co-Authored-By: Claude 81847+claude@users.noreply.github.com