/* The deck engine and shared components. Scene styles go in the scene's own
   scene.css, scoped under [data-scene="NN-name"]. */

* { box-sizing: border-box; }
html, body { margin: 0; height: 100%; background: var(--letterbox); color: var(--ink); }
body { font-family: var(--sans); -webkit-font-smoothing: antialiased; text-rendering: optimizeLegibility; overflow: hidden; }
code, .code, pre, .mono { font-family: var(--mono); font-variant-ligatures: none; font-feature-settings: "liga" 0, "calt" 0; }
/* `code` (ctx.fmt) never shows ligatures such as `===`, even under a scene rule
   whose `font` shorthand resets the ligature settings. */
code { font-variant-ligatures: none !important; }

/* Stage ------------------------------------------------------------------ */
#viewport { position: fixed; inset: 0; overflow: hidden; }
.stage { position: absolute; left: 0; top: 0; width: 1920px; height: 1080px; transform-origin: 0 0;
  background: var(--page); overflow: hidden; font-size: var(--t-body); line-height: 1.3; }
.stage.instant, .stage.instant * { transition: none !important; animation: none !important; }
.scene { position: absolute; inset: 0; }
.scene:not(.is-current) { display: none; }
body.blank .stage > * { visibility: hidden !important; }

/* Header: the title, top left. Drawn by the engine. */
.scene-header { position: absolute; left: var(--margin-x); right: var(--margin-x); top: var(--header-top);
  display: flex; align-items: baseline; gap: 28px; }
.scene-title { font: 600 var(--t-title)/1.08 var(--serif); letter-spacing: -0.02em; margin: 0; color: var(--ink);
  font-feature-settings: "kern", "liga", "lnum"; }
.scene-title code { font-size: .84em; font-weight: 500; letter-spacing: 0; }
.scene-header { transition: opacity var(--t-move) var(--ease), visibility 0s; }
.scene-header.is-off { opacity: 0; visibility: hidden; transition: opacity var(--t-move) var(--ease), visibility 0s linear var(--t-move); }

/* The progress bar: one segment per part across the top edge, labelled;
   the current part filled. Drawn by the engine over every scene. */
.stage-progress { position: absolute; left: var(--margin-x); right: var(--margin-x); top: 24px; display: flex; gap: 10px; z-index: 4;
  pointer-events: none; transition: opacity 400ms var(--ease); }
.stage-progress[hidden] { display: none; }
.stage-progress.off { opacity: 0; }
.progress-part { flex: 1; min-width: 0; }
.progress-bar { height: 3px; border-radius: 2px; background: var(--rule-soft); transition: background-color 400ms var(--ease); }
.progress-part.done .progress-bar { background: var(--rule); }
.progress-part.current .progress-bar { background: var(--ink); }
.progress-label { margin-top: 10px; font: 600 var(--t-min)/1 var(--sans); letter-spacing: .12em; text-transform: uppercase; color: var(--muted); }
.progress-part.current .progress-label { color: var(--ink); }

/* A part divider: a short pause between parts. The part's number large and
   faint behind its title, and nothing else. */
.scene.divider { background: var(--page); }
.divider-card { position: absolute; left: 216px; right: 216px; top: 440px; }
.divider-numeral { position: absolute; right: -20px; top: -200px; font: 400 400px/1 var(--serif); letter-spacing: -0.04em;
  color: var(--numeral); pointer-events: none; }
.divider-kicker { position: relative; font: 600 var(--t-label)/1 var(--sans); letter-spacing: .22em; text-transform: uppercase; color: var(--muted); }
.divider-title { position: relative; font: 600 var(--t-display)/1 var(--serif); letter-spacing: -0.025em; margin: 22px 0 0; color: var(--ink);
  max-width: 1280px; }  /* a long title wraps before it reaches the numeral */

/* Step states. Every [data-step] element gets .is-on or .is-off; off means
   invisible. `.rise` also slides up a little as it appears. */
[data-step] { transition: opacity var(--t-fast) var(--ease), transform var(--t-fast) var(--ease), visibility 0s linear 0s; }
[data-step].is-off { opacity: 0; visibility: hidden;
  transition: opacity var(--t-fast) var(--ease), transform var(--t-fast) var(--ease), visibility 0s linear var(--t-fast); }
/* An element that holds a dark code slab fades in two halves, so that a
   half-faded slab never shows as a grey block on the page: its ground comes
   in over the first 30% of --t-fast (the engine fades the slab's contents
   in over the second half), and goes out over the last 30% (the contents
   fade over the first half). Two slabs swapped in place keep a dark ground
   throughout. See lib/motion.js, "Dark code slabs". (:where keeps the
   specificity of the rules above, so a scene's own transition still wins.) */
[data-step]:where(.code-panel:not(.bare), :has(.code-panel:not(.bare) > .code-box)) {
  transition: opacity calc(var(--t-fast) * .3) var(--ease), transform var(--t-fast) var(--ease), visibility 0s linear 0s; }
[data-step]:where(.code-panel:not(.bare), :has(.code-panel:not(.bare) > .code-box)).is-off {
  transition: opacity calc(var(--t-fast) * .3) var(--ease) calc(var(--t-fast) * .7), transform var(--t-fast) var(--ease), visibility 0s linear var(--t-fast); }
/* The contents of a slab (lib/motion.js, fadeSlabContents): their opacity
   is --slab-content, which the engine animates on the element that fades. */
@property --slab-content { syntax: '<number>'; inherits: true; initial-value: 1; }
.code-panel:not(.bare) > .code-box > * { opacity: var(--slab-content); }
/* A slab's file:line caption, on the page under it, goes with the contents,
   so that two slabs swapped in place never show both captions. */
.code-panel:not(.bare) > .code-caption { opacity: var(--slab-content); }
/* SVG groups keep their own transforms: fade only. */
svg [data-step] { transition: opacity var(--t-fast) var(--ease), visibility 0s linear 0s; }
.rise.is-off { transform: translateY(14px); }
body.blank .stage { background: #000; }

/* Chrome outside the stage: hints, index overlay, help, lint. Hidden in
   print and mirror views. */
.deck-badge { position: fixed; right: 12px; bottom: 10px; font: 600 13px/1 var(--sans); color: #c9ced4; background: #2a2d31;
  border-radius: 4px; padding: 5px 8px; opacity: .85; z-index: 20; }
.deck-badge:empty { display: none; }
.overlay { position: fixed; inset: 0; background: rgba(20, 22, 25, .94); color: #eef1f4; z-index: 30; overflow: auto; padding: 40px 56px;
  font: 400 17px/1.4 var(--sans); }
.overlay[hidden] { display: none; }
.overlay h2 { font: 600 26px/1.2 var(--serif); margin: 0 0 20px; }
.index-grid { display: grid; grid-template-columns: repeat(auto-fill, minmax(300px, 1fr)); gap: 14px; }
.index-card { text-align: left; border: 1px solid #454a50; background: #24272b; color: inherit; border-radius: 6px; padding: 12px 14px;
  font: inherit; cursor: pointer; min-height: 116px; display: flex; flex-direction: column; gap: 6px; }
.index-card:hover, .index-card:focus-visible { border-color: #9fb4c8; outline: none; background: #2c3035; }
.index-card.current { border-color: #e8eef4; box-shadow: 0 0 0 1px #e8eef4; }
.index-card .n { font: 500 14px/1 var(--mono); color: #aab2bb; }
.index-card .t { font: 600 19px/1.25 var(--sans); }
.index-card .m { font-size: 14px; color: #aab2bb; margin-top: auto; }
.index-card.planned .t { color: #aab2bb; }
.index-card.broken .n { color: #ff9c94; }
.index-total { margin-top: 18px; color: #aab2bb; font-size: 15px; }
.index-head { display: flex; align-items: baseline; gap: 24px; flex-wrap: wrap; margin-bottom: 20px; }
.index-head h2 { margin: 0; }
.index-goto { font: 500 16px/1 var(--mono); color: #eef1f4; background: #24272b; border: 1px solid #454a50; border-radius: 6px;
  padding: 8px 10px; width: 340px; max-width: 100%; }
.index-goto:focus { outline: none; border-color: #9fb4c8; }
.index-goto.bad { border-color: #ff9c94; }
.overlay h2.index-backup { margin: 30px 0 14px; }
.help-keys { display: grid; grid-template-columns: max-content 1fr; gap: 6px 22px; font-size: 18px; }
.help-keys kbd { font: 500 16px/1 var(--mono); border: 1px solid #5b6168; border-radius: 4px; padding: 3px 7px; background: #2c3035; }

.lint { position: fixed; left: 10px; bottom: 10px; max-width: min(760px, 70vw); max-height: 45vh; overflow: auto; z-index: 25;
  background: #fff6f5; color: #5b0f0a; border: 2px solid var(--rejected-ink); border-radius: 6px; padding: 10px 14px;
  font: 400 14px/1.45 var(--sans); box-shadow: 0 6px 24px rgba(0, 0, 0, .25); }
.lint.ok { background: #f1f8f3; color: #0f4424; border-color: var(--proved-ink); }
.lint h3 { font: 700 14px/1.3 var(--sans); margin: 0 0 6px; }
.lint ul { margin: 0; padding-left: 18px; }
.lint code { font-size: 13px; }

/* Placeholder and error cards for scenes that are not built. */
.scene-placeholder { position: absolute; left: var(--margin-x); right: var(--margin-x); top: 420px; font: 400 var(--t-body)/1.4 var(--sans);
  color: var(--muted); border-top: 2px dashed var(--rule); padding-top: 28px; display: flex; gap: 28px; align-items: baseline; }
.scene-placeholder .ph-id { font: 500 var(--t-label)/1 var(--mono); color: var(--ink-2); }
.scene-placeholder.error { color: var(--rejected-ink); border-top-color: var(--rejected-edge); white-space: pre-wrap; font-size: var(--t-label); display: block; }

/* Print: one 1920x1080 page per step. */
body.print { overflow: auto; background: #6b7077; height: auto; }
body.print #viewport { position: static; }
.print-page { position: relative; width: 1920px; height: 1080px; overflow: hidden; margin: 0 auto 24px; background: var(--page); }
.print-page > .stage { position: absolute; transform: none; }
.print-label { position: absolute; right: 18px; bottom: 8px; font: 400 14px/1 var(--mono); color: #8b949d; z-index: 5; }
@page { size: 1920px 1080px; margin: 0; }
@media print {
  body.print { background: none; }
  .print-page { margin: 0; break-after: page; zoom: 1 !important; }
  .deck-badge, .lint { display: none !important; }
}

/* Components ---------------------------------------------------------- */

/* Code panel. Geometry is in `ch` and `lh` of the panel's own font, so that
   marks can be placed by line and column. */
.code-panel { position: relative; --lh: 1.45; }
.code-panel .code-box { position: relative; background: var(--code-bg); border: 1px solid var(--code-edge); border-radius: var(--radius);
  padding: .72em 1.05em; overflow: hidden; color: var(--ink);
  box-shadow: 0 1px 0 rgba(255, 255, 255, .05) inset, 0 2px 4px rgba(20, 16, 10, .10), 0 24px 48px -16px rgba(20, 16, 10, .35); }
.code-panel.bare .code-box { background: none; border: 0; padding: 0; box-shadow: none; }
.code-panel pre { margin: 0; font-size: inherit; line-height: var(--lh); white-space: pre; color: var(--syn-ident); position: relative; }
.code-panel.size-l { font-size: var(--t-code); }
.code-panel.size-m { font-size: var(--t-code-s); }
.code-panel.size-s { font-size: var(--t-code-xs); }
.code-panel .ln { display: block; height: calc(var(--lh) * 1em); position: relative; z-index: 1; }
.code-panel .window { overflow: hidden; position: relative; }
.code-panel .scroller { transition: transform var(--t-move) var(--ease); will-change: transform; }
.code-caption { margin-top: 14px; font: 400 var(--t-min)/1.2 var(--mono); color: var(--muted); display: flex; gap: 18px; flex-wrap: wrap; }
.code-caption[hidden] { display: none; }
.code-caption a { color: inherit; text-decoration: none; border-bottom: 1px solid var(--rule); }
.code-caption .note { font-family: var(--sans); }

/* Syntax classes (tok-*): weight and grey only. */
.tok-keyword { color: var(--syn-keyword); font-weight: 700; }
.tok-vox { color: var(--syn-keyword); font-weight: 700; }
.tok-constructor { color: var(--syn-constructor); }
.tok-mode { color: var(--syn-mode); font-weight: 500; }
.tok-attr { color: var(--syn-mode); font-weight: 500; }
.tok-operator { color: var(--syn-operator); }
.tok-string { color: var(--syn-string); }
.tok-number { color: var(--syn-number); }
.tok-comment { color: var(--syn-comment); font-style: italic; }
.tok-punct { color: var(--syn-punct); }
.tok-refine { color: var(--spec-ink); font-weight: 700; }
.tok-pred { color: var(--spec-ink); }
.tok-var { color: var(--ink-2); }
.tok-symbol { color: var(--syn-constructor); }
.tok-elided { color: var(--muted); }
.tok-location { color: var(--ink); font-weight: 500; }
.tok-error { color: var(--rejected-ink); font-weight: 700; }
.tok-warning { color: var(--assumed-ink); font-weight: 700; }
.tok-caret { color: var(--rejected-ink); font-weight: 700; }
.tok-prompt { color: var(--muted); }

/* Ghost text: tinted while .ghost-tint is on the panel, faded (erased) when
   .ghost-faded is on. */
.code-panel .g { transition: color var(--t-fade) var(--ease), opacity var(--t-fade) var(--ease), background-color var(--t-fade) var(--ease); }
.code-panel.ghost-tint .g, .code-panel.ghost-tint .g span { color: var(--ghost-ink); }
.code-panel.ghost-tint .g { background: var(--ghost-tint); border-radius: .14em; }
.code-panel.ghost-faded .g { opacity: .16; background: none; }

/* Marks: rectangles behind the text, positioned in ch/lh. They reach .2em
   past the text on each side, so a box's edge clears a wide glyph at its
   ends (`{`, `}`, `e`); the text itself does not move. Where a character
   touches the marked text, that side stops at the cell's edge (--pad-l,
   --pad-r: lib/code.js, markPad). */
.mark { --pad-l: .2em; --pad-r: .2em; position: absolute; z-index: 0; left: calc(var(--col) * 1ch - var(--pad-l)); top: calc(var(--row) * var(--lh) * 1em);
  width: calc(var(--len) * 1ch + var(--pad-l) + var(--pad-r)); height: calc(var(--lh) * 1em); border-radius: .22em; pointer-events: none;
  transition: opacity var(--t-fast) var(--ease); }
.mark.is-off { opacity: 0; }
.mark.box { background: var(--mc-tint); box-shadow: inset 0 0 0 1.5px var(--mc-edge); }
.mark.fill { background: var(--mc-tint); }
.mark.under::after { content: ""; position: absolute; left: var(--pad-l); right: var(--pad-r); bottom: .04em; height: 3px; background: var(--mc-ink); border-radius: 2px; }
.mark.line { left: -.5em; width: calc(100% + 1em); background: var(--mc-tint); border-left: 4px solid var(--mc-ink); border-radius: 0; }
.mark.m-spec { --mc-ink: var(--spec-ink); --mc-tint: var(--spec-tint); --mc-edge: var(--spec-edge); }
.mark.m-ghost { --mc-ink: var(--ghost-ink); --mc-tint: var(--ghost-tint); --mc-edge: var(--ghost-edge); }
.mark.m-proved { --mc-ink: var(--proved-ink); --mc-tint: var(--proved-tint); --mc-edge: var(--proved-edge); }
.mark.m-tested { --mc-ink: var(--tested-ink); --mc-tint: var(--tested-tint); --mc-edge: var(--tested-edge); }
.mark.m-assumed { --mc-ink: var(--assumed-ink); --mc-tint: var(--assumed-tint); --mc-edge: var(--assumed-edge); }
.mark.m-rejected { --mc-ink: var(--rejected-ink); --mc-tint: var(--rejected-tint); --mc-edge: var(--rejected-edge); }
.mark.m-unclaimed { --mc-ink: var(--unclaimed-ink); --mc-tint: var(--unclaimed-tint); --mc-edge: var(--unclaimed-edge); }
.mark.m-focus { --mc-ink: var(--focus-edge); --mc-tint: var(--focus-tint); --mc-edge: var(--focus-edge); }
/* An obligation (V2): what must be proved where a value meets a refined
   type. An amber outline with no fill, so that it reads apart from the
   filled `assumed` mark, which means trusted. */
.mark.m-obligation { --mc-ink: var(--assumed-ink); --mc-tint: transparent; --mc-edge: var(--assumed-ink); }
.mark.box.m-obligation { background: none; box-shadow: inset 0 0 0 2.5px var(--mc-edge); }

/* Lines revealed step by step. */
.code-panel .ln.is-off { opacity: 0; }
.code-panel .ln { transition: opacity var(--t-fast) var(--ease); }
.code-panel .ln.cut { color: var(--muted); font-family: var(--sans); font-style: italic; }

/* Diff lines: neutral, so as not to claim anything. */
.code-panel .ln.d-del { text-decoration: line-through; text-decoration-color: var(--muted); color: var(--muted); }
.code-panel .ln.d-del * { color: var(--muted) !important; }
.code-panel .ln.d-add { background: var(--focus-tint); }

/* Compiler output. */
.output-panel .code-box { background: var(--code-bg); }
.verdict { display: inline-flex; align-items: center; gap: 10px; font: 600 var(--t-label)/1 var(--sans); padding: 7px 14px; border-radius: 18px; }
.verdict.accepted { color: var(--proved-ink); background: var(--proved-tint); }
.verdict.rejected { color: var(--rejected-ink); background: var(--rejected-tint); }
.verdict.recorded { color: var(--ink-2); background: var(--unclaimed-tint); }

/* Side by side. */
.side-by-side { display: grid; gap: var(--s5); align-items: start; }
.side-by-side > * { min-width: 0; }

/* Limits strip: four fixed columns, fixed colours, fixed order. */
.limits-strip { position: absolute; left: var(--margin-x); right: var(--margin-x); top: var(--strip-top); height: var(--strip-h);
  display: grid; grid-template-columns: repeat(4, 1fr); gap: 28px; }
.limits-strip .col { border-top: 3px solid var(--c-ink); padding-top: 12px; min-width: 0; }
.limits-strip .col.proved { --c-ink: var(--proved-ink); }
.limits-strip .col.tested { --c-ink: var(--tested-ink); }
.limits-strip .col.assumed { --c-ink: var(--assumed-ink); }
.limits-strip .col.unclaimed { --c-ink: var(--unclaimed-ink); }
.limits-strip h4 { margin: 0 0 7px; font: 700 var(--t-min)/1 var(--sans); letter-spacing: .12em; text-transform: uppercase; color: var(--c-ink); }
.limits-strip p { margin: 0; font: 400 var(--t-min)/1.28 var(--sans); color: var(--ink-2); }
.limits-strip p.none { color: var(--muted); }
.limits-strip code { font-size: 1em; }

/* Evidence words in running text: proved / tested / assumed. */
.ev { font-weight: 700; }
.ev.proved { color: var(--proved-ink); }
.ev.tested { color: var(--tested-ink); }
.ev.assumed { color: var(--assumed-ink); }
.ev.rejected { color: var(--rejected-ink); }
.ev.unclaimed { color: var(--unclaimed-ink); }

/* Callouts: a label attached to a line of a code panel. */
.callout { position: absolute; font: 400 var(--t-body)/1.25 var(--sans); color: var(--ink); max-width: 560px; }
.callout code { font-size: .88em; }
.callout::before { content: ""; position: absolute; left: -26px; top: .6em; width: 16px; height: 3px; background: var(--focus-edge); }
.callout.m-ghost::before { background: var(--ghost-ink); }
.callout.m-spec::before { background: var(--spec-ink); }

/* Tables with row reveal. */
.deck-table { border-collapse: collapse; font: 400 var(--t-body)/1.25 var(--sans); width: 100%; }
.deck-table th { text-align: left; font: 700 var(--t-label)/1.2 var(--sans); color: var(--muted); border-bottom: 1.5px solid var(--ink);
  padding: 0 18px 10px 0; letter-spacing: .02em; }
.deck-table td { border-bottom: 1px solid var(--rule-soft); padding: 14px 18px 14px 0; vertical-align: top; }
.deck-table tr.row { transition: opacity var(--t-fast) var(--ease), background-color var(--t-fast) var(--ease); }
.deck-table tr.row.is-off { opacity: 0; }
.deck-table tr.row.latest td { background: var(--focus-tint); }
.deck-table code { font-size: .88em; }

/* Diagrams. */
svg.diagram { overflow: visible; font-family: var(--sans); }
svg.diagram .box rect { fill: var(--surface); stroke: var(--surface-edge); stroke-width: 1.5; }
svg.diagram .box text { font-size: 28px; fill: var(--ink); }
svg.diagram .box text.sub, svg.diagram .arrow-label { font-size: 22px; fill: var(--muted); }
svg.diagram .box.spec rect { fill: var(--spec-tint); stroke: var(--spec-edge); }
svg.diagram .box.ghost rect { fill: var(--ghost-tint); stroke: var(--ghost-edge); }
svg.diagram .box.focus rect { fill: var(--focus-tint); stroke: var(--focus-edge); }
svg.diagram .box.muted rect { fill: var(--surface-2); stroke: var(--surface-edge); }
svg.diagram .box.proved rect { fill: var(--proved-tint); stroke: var(--proved-edge); }
svg.diagram .box.assumed rect { fill: var(--assumed-tint); stroke: var(--assumed-edge); }
svg.diagram .chip line { transform-box: fill-box; transform-origin: left center; }
svg.diagram text.mono { font-family: var(--mono); }
svg.diagram .arrow { fill: none; stroke: var(--ink-2); stroke-width: 2; stroke-linecap: round; }
svg.diagram .arrowhead { fill: var(--ink-2); }
svg.diagram .chip rect { stroke-width: 2; }
svg.diagram .chip text { font-family: var(--mono); font-size: 24px; }
svg.diagram .chip.ghost rect { fill: var(--ghost-tint); stroke: var(--ghost-edge); } svg.diagram .chip.ghost text { fill: var(--ghost-ink); }
svg.diagram .chip.spec rect { fill: var(--spec-tint); stroke: var(--spec-edge); } svg.diagram .chip.spec text { fill: var(--spec-ink); }
svg.diagram .chip.plain rect { fill: var(--surface-2); stroke: var(--surface-edge); } svg.diagram .chip.plain text { fill: var(--ink); }
svg.diagram .chip.consumed { opacity: .25; }
svg.diagram .chip.consumed line { stroke: var(--ink-2); stroke-width: 2.5; }
svg.diagram .cell rect { fill: var(--surface); stroke: var(--surface-edge); stroke-width: 1.5; }
svg.diagram .cell .addr { font: 400 22px var(--mono); fill: var(--muted); }
svg.diagram .cell .val { font: 500 26px var(--mono); fill: var(--ink); }
svg.diagram .lattice .axis text { font-size: 22px; fill: var(--muted); }
svg.diagram .lattice .axis .name { font-weight: 600; fill: var(--ink-2); }
svg.diagram .lattice .axis line { stroke: var(--rule); stroke-width: 2; }
svg.diagram .lattice .axis circle { fill: var(--page); stroke: var(--muted); stroke-width: 2; }
svg.diagram .lattice .axis.new text { fill: var(--ink); }
svg.diagram .lattice .axis.new .name { fill: var(--ink); }
svg.diagram .lattice .axis.new line { stroke: var(--ink); stroke-width: 3; }
svg.diagram .lattice .axis.new circle { fill: var(--ink); stroke: var(--ink); }
svg.diagram .lattice .axis.new rect.band { fill: var(--focus-tint); }
svg.diagram .reveal { transition: opacity var(--t-fast) var(--ease); }
svg.diagram .reveal.is-off { opacity: 0; }

/* Live embed. */
.live-embed { position: relative; border: 1.5px solid var(--surface-edge); border-radius: var(--radius); overflow: hidden; background: var(--page); }
.live-embed iframe { border: 0; width: 100%; height: 100%; display: block; background: var(--page); }
.live-embed .live-status { position: absolute; right: 12px; top: 10px; z-index: 3; font: 600 var(--t-min)/1 var(--sans); }
.live-embed.fallback iframe { visibility: hidden; }
.live-embed .recorded { position: absolute; inset: 0; background: var(--page); padding: 20px 24px; display: none; overflow: hidden; }
.live-embed.fallback .recorded { display: grid; grid-template-columns: 1fr 1fr; gap: 24px; align-content: start; }
.live-embed .recorded .label { grid-column: 1 / -1; font: 400 var(--t-min)/1.2 var(--sans); color: var(--muted); }
.live-embed.stacked.fallback .recorded { grid-template-columns: minmax(0, 1fr); gap: 10px; }

/* Code panel: scrolling window track, callouts, gutter. */
.code-panel .rows { align-items: flex-start; }
.code-panel pre.gutter-col { flex: none; margin-right: 1.4ch; text-align: right; color: var(--muted); }
.code-panel pre.gutter-col .gutter { user-select: none; }
.code-panel pre.code { flex: 1; min-width: 0; }
.code-panel .track { position: absolute; right: 6px; top: .55em; bottom: .55em; width: 6px; border-radius: 3px; background: var(--rule-soft); }
.code-panel .thumb { position: absolute; left: 0; right: 0; border-radius: 3px; background: var(--muted);
  transition: top var(--t-move) var(--ease), height var(--t-move) var(--ease); }
.callout-layer { position: absolute; left: 0; top: 0; width: 0; height: 0; }
.callout { transform: translateY(-50%); width: max-content; max-width: 500px; transition: opacity var(--t-fast) var(--ease), top var(--t-move) var(--ease); }
.callout::before { display: none; }
svg.callout-leaders { position: absolute; left: 0; top: 0; overflow: visible; pointer-events: none; }
.callout-leader { fill: none; stroke: var(--focus-edge); stroke-width: 2; stroke-linecap: round; transition: opacity var(--t-fast) var(--ease); }
.callout-leader.m-ghost { stroke: var(--ghost-ink); }
.callout-leader.m-spec { stroke: var(--spec-ink); }
.callout-leader.m-proved { stroke: var(--proved-ink); }
.callout-leader.m-tested { stroke: var(--tested-ink); }
.callout-leader.m-assumed { stroke: var(--assumed-ink); }
.callout-leader.m-rejected { stroke: var(--rejected-ink); }
.callout-leader.m-unclaimed { stroke: var(--unclaimed-ink); }
.callout.out-of-window, .callout-leader.out-of-window { opacity: 0 !important; visibility: hidden; }

/* Autoplay: the start cover (outside the stage). */
.play-cover { position: fixed; left: 50%; bottom: 7vh; transform: translateX(-50%); z-index: 40; border: 0; cursor: pointer;
  background: rgba(21, 25, 30, .86); color: #fff; border-radius: 40px; padding: 16px 30px; display: flex; gap: 16px; align-items: baseline;
  font: 600 22px/1 var(--sans); box-shadow: 0 10px 40px rgba(0, 0, 0, .3); }
.play-cover small { font-weight: 400; font-size: 15px; color: #c6ccd3; }
.play-cover[hidden] { display: none; }
body.mode-render .deck-badge, body.mode-render .lint, body.mode-render .overlay { display: none !important; }

/* Motion primitives (lib/morph.js, lib/figures.js). -------------------- */

/* Code morph: tokens placed on a character grid. */
.code-panel.morph .morph-body { position: relative; line-height: var(--lh); white-space: pre; font-family: var(--mono); color: var(--syn-ident);
  font-variant-ligatures: none; font-feature-settings: "liga" 0, "calt" 0; }
.code-panel.morph .atom { position: absolute; left: calc(var(--col) * 1ch); top: calc(var(--row) * var(--lh) * 1em);
  line-height: var(--lh); white-space: pre; z-index: 1; }
.code-panel.morph .atom.gone { opacity: 0; visibility: hidden; }
/* A morph whose values fly in from outside it (a substitution with `from`)
   does not clip them; a morph never scrolls. */
.code-panel.morph.flies-in .code-box, .code-panel.morph.flies-in .window { overflow: visible; }
.code-panel.morph .atom.g { color: var(--ghost-ink); background: var(--ghost-tint); box-shadow: 0 0 0 .08em var(--ghost-tint); border-radius: .12em; }
.code-panel.morph .atom.g span, .code-panel.morph .atom.g.tok-vox, .code-panel.morph .atom.g.tok-keyword { color: var(--ghost-ink); }
.code-panel.morph .mark { z-index: 0; }

.fig { position: absolute; }
.fig .gone, .fig.gone { opacity: 0; visibility: hidden; }

/* A value put in by a substitution is marked where it lands, in the
   neutral "look here" colour (a substitution may be a counterexample or an
   argument at a call). */
.code-panel.morph .atom.sub { background: var(--focus-tint); border-radius: .16em; box-shadow: 0 0 0 .1em var(--focus-tint); font-weight: 700; }

/* Figures scale with their geometry: each primitive sets its size on its
   element (--hm-row, --tk, --as-h) and the type follows, never below the
   sizes the deck used before. */

/* Heap map (V6): a card; the header names the permission, its mode word
   (`own`) set apart; each row maps a cell (a chip) to its value. */
.heap-map { --hm-row: 92px; --hm-head: 77px; }
.heap-map .hm-table { position: absolute; border: 1.5px solid var(--surface-edge); border-radius: 16px; background: var(--surface);
  box-shadow: var(--lift); overflow: hidden; }
.heap-map .hm-head { height: calc(var(--hm-head) - 3px); padding: 0 .8em; display: flex; align-items: center; white-space: nowrap;
  border-bottom: 1.5px solid var(--surface-edge); background: var(--surface-2);
  font: 500 max(var(--t-label), calc(var(--hm-head) * .4))/1 var(--mono); color: var(--ink); }
.heap-map .hm-mode { color: var(--muted); font-weight: 400; }
.heap-map .hm-name { color: var(--ink); font-weight: 700; margin-left: .6ch; }
.heap-map.kind-ghost .hm-table { border-color: var(--ghost-edge); }
.heap-map.kind-ghost .hm-head { background: var(--ghost-tint); border-bottom-color: var(--ghost-edge); }
.heap-map.kind-ghost .hm-mode { color: var(--ghost-ink); opacity: .8; }
.heap-map.kind-ghost .hm-name { color: var(--ghost-ink); }
.heap-map .hm-row { position: absolute; border-bottom: 1px solid var(--rule-soft); transition: background-color var(--t-fast) var(--ease); }
.heap-map .hm-row.changed { background: var(--focus-tint); box-shadow: inset 4px 0 0 var(--focus-edge); }
.heap-map .hm-key { position: absolute; left: 0; top: 0; bottom: 0; display: flex; align-items: center; padding-left: max(16px, calc(var(--hm-row) * .22)); }
.heap-map .hm-chip { font: 700 max(var(--t-label), calc(var(--hm-row) * .39))/1 var(--mono); color: var(--ink); background: var(--surface-2);
  border: 1.5px solid var(--surface-edge); border-radius: 8px; padding: .22em .45em .26em; white-space: nowrap; }
.heap-map .hm-maps { position: absolute; top: 50%; width: calc(var(--hm-row) * .36); height: 2.5px; margin: -1px 0 0 max(8px, calc(var(--hm-row) * .1));
  background: var(--muted); z-index: 1; }
.heap-map .hm-maps::before { content: ""; position: absolute; left: 0; top: -7px; width: 2px; height: 16px; background: var(--muted); }
.heap-map .hm-maps::after { content: ""; position: absolute; right: -1px; top: -5px; border: 6px solid transparent; border-right: 0; border-left: 9px solid var(--muted); }
.heap-map .hm-val { position: absolute; top: 0; bottom: 0; overflow: hidden; }
.heap-map .hm-v { position: absolute; left: calc(max(8px, var(--hm-row) * .1) + var(--hm-row) * .36 + 14px); top: 50%; margin-top: -.62em;
  font: 500 max(var(--t-code-s), calc(var(--hm-row) * .41))/1.2 var(--mono); color: var(--ink); white-space: nowrap; }

/* Permission token (V7): a ticket. A notched card with a perforated stub,
   filled with the ghost colour, its name in white; the lent copy is its
   dashed outline; a stale token has a red ring. */
.token-layer { position: absolute; inset: 0; pointer-events: none; }
.token { --tk: 88px; position: absolute; left: 0; top: 0; display: flex; align-items: center; justify-content: center;
  padding-left: calc(var(--tk) * .19); font: 700 max(var(--t-label), calc(var(--tk) * .41))/1 var(--mono); white-space: nowrap; color: var(--token-text); }
.token .tk-shape { position: absolute; left: 0; top: 0; overflow: visible; filter: var(--token-glow); }
.token .tk-text { position: relative; }
.token .tk-body { stroke: var(--token-edge); stroke-width: 1.5; }
.token .tk-g0 { stop-color: var(--token-g0); }
.token .tk-g1 { stop-color: var(--token-g1); }
.token .tk-perf { stroke: var(--token-text); stroke-width: 2; stroke-dasharray: 2 4.5; stroke-linecap: round; opacity: .55; fill: none; }
.token .tk-shine { stroke: #fff; stroke-width: 1.5; opacity: .3; stroke-linecap: round; }
.token.kind-spec { --token-g0: var(--spec-ink); --token-g1: var(--spec-edge); --token-edge: var(--spec-ink); }
.token.kind-plain { --token-g0: var(--surface); --token-g1: var(--surface-2); --token-edge: var(--ink-2); --token-text: var(--ink); }
.token.lent { color: var(--ghost-ink); }
.token.lent .tk-shape { filter: none; }
.token.lent .tk-body { fill: var(--page); fill-opacity: .7; stroke: var(--ghost-ink); stroke-width: 2; stroke-dasharray: 6 5; }
.token.lent .tk-perf { stroke: var(--ghost-ink); }
.token.lent .tk-shine { display: none; }
.token.stale .tk-body { stroke: var(--rejected-ink); stroke-width: 3; }
.token.stale .tk-shape { filter: drop-shadow(0 0 10px var(--rejected-edge)); }
.token.gone, .token-layer .gone { opacity: 0; visibility: hidden; }
.tk-tether-svg { position: absolute; left: 0; top: 0; overflow: visible; }
.tk-tether { fill: none; stroke: var(--ghost-ink); stroke-width: 2; stroke-dasharray: 1 7; stroke-linecap: round; opacity: .8; }
.fig-box { border: 1.5px solid var(--surface-edge); border-radius: 16px; background: var(--surface); display: flex; flex-direction: column;
  align-items: center; justify-content: center; gap: 6px; box-shadow: var(--lift); }
.fig-box .fb-label { font: 600 var(--t-body)/1.1 var(--sans); color: var(--ink); }
.fig-box .fb-label code { font-weight: 500; }
.fig-box .fb-sub { font: 400 var(--t-min)/1.2 var(--sans); color: var(--muted); }
.fig-box.label-top { justify-content: flex-start; padding-top: 22px; }

/* Array slice (V8): one continuous bar per run of cells, rounded at its
   ends; below it the final row as a dashed violet prophecy; a dashed cut
   between the halves of a split. */
.array-slice { --as-h: 128px; }
.array-slice .as-cell { position: absolute; border: 1.5px solid var(--surface-edge); border-left-width: 0; background: var(--surface);
  display: grid; place-items: center; transition: background-color var(--t-fast) var(--ease); }
.array-slice .as-cell.edge-l { border-left-width: 1.5px; border-radius: 14px 0 0 14px; }
.array-slice .as-cell.edge-r { border-radius: 0 14px 14px 0; }
.array-slice .as-cell.edge-l.edge-r { border-radius: 14px; }
.array-slice .as-cell.changed { background: var(--focus-tint); }
.array-slice .as-val { font: 500 max(var(--t-code), calc(var(--as-h) * .36))/1 var(--mono); color: var(--ink); }
.array-slice .as-idx { position: absolute; left: 10px; top: 8px; font: 400 var(--t-min)/1 var(--mono); color: var(--muted); }
.array-slice .as-final { position: absolute; display: grid; place-items: center; overflow: hidden;
  background: transparent; border: 2px dashed var(--ghost-edge); border-left-width: 0; }
.array-slice .as-final.edge-l { border-left-width: 2px; border-radius: 14px 0 0 14px; }
.array-slice .as-final.edge-r { border-radius: 0 14px 14px 0; }
.array-slice .as-final.edge-l.edge-r { border-radius: 14px; }
.array-slice .as-final.known { background: var(--ghost-tint); }
.array-slice .as-final span { font: 500 max(var(--t-code), calc(var(--as-h) * .36))/1 var(--mono); color: var(--ghost-edge); }
.array-slice .as-final.known span { color: var(--ghost-ink); font-weight: 700; }
.array-slice .as-label { position: absolute; right: 100%; margin-right: 24px; transform: translateY(-50%); white-space: nowrap;
  font: 600 max(var(--t-min), calc(var(--as-h) * .19))/1 var(--sans); letter-spacing: .12em; text-transform: uppercase; color: var(--muted); }
.array-slice .as-final-label { color: var(--ghost-ink); }
.array-slice .as-bracket { position: absolute; height: 16px; border: 2px solid var(--ink-2); border-top: 0; border-radius: 0 0 4px 4px; transform-origin: center top; }
.array-slice .as-bracket span { position: absolute; left: 0; right: 0; top: 28px; text-align: center; white-space: nowrap;
  font: 600 max(var(--t-min), calc(var(--as-h) * .19))/1 var(--sans); color: var(--ink-2); letter-spacing: .02em; }
.array-slice .as-cut { position: absolute; width: 0; border-left: 2px dashed var(--muted); transform-origin: center top; margin-left: -1px; }

/* Counterexample card (V3): the card the values fly from. */
.cex-card { background: var(--surface); border: 1.5px solid var(--rejected-edge); border-radius: var(--radius); padding: 16px 26px 18px;
  box-shadow: var(--lift), inset 4px 0 0 var(--rejected-ink); }
.cex-card .cex-title { font: 600 var(--t-min)/1 var(--sans); letter-spacing: .12em; text-transform: uppercase; color: var(--rejected-ink); margin-bottom: 12px; }
.cex-card .cex-row { font: 500 30px/1.5 var(--mono); color: var(--ink); white-space: nowrap; }
.cex-card .cex-eq { color: var(--muted); margin: 0 .5ch; }
.cex-card .cex-val { color: var(--rejected-ink); font-weight: 700; }

/* Demo grid (V9). */
.demo-grid .dg-card { position: absolute; border: 1.5px solid var(--surface-edge); border-radius: 12px; background: var(--surface); padding: 11px 14px;
  transition: opacity var(--t-move) var(--ease), background-color var(--t-fast) var(--ease), border-color var(--t-fast) var(--ease); overflow: hidden; }
.demo-grid .dg-card.dim { opacity: .3; }
.demo-grid .dg-card.gone { opacity: 0; visibility: hidden; }
.demo-grid .dg-card.lit { border-color: var(--ink-2); box-shadow: var(--lift); }
.demo-grid .dg-title { font: 600 24px/1.1 var(--sans); color: var(--ink); }
.demo-grid .dg-line { margin-top: 5px; font: 400 var(--t-min)/1.15 var(--sans); color: var(--ink-2); }
.demo-grid .dg-badge { position: absolute; right: 10px; bottom: 10px; font: 600 var(--t-min)/1 var(--sans); color: var(--proved-ink);
  background: var(--proved-tint); border-radius: 12px; padding: 4px 10px; }
.demo-grid .dg-badge[hidden] { display: none; }
.demo-grid.mini .dg-card { padding: 0; border-radius: 3px; box-shadow: none; background: var(--rule-soft); border: 0; }
.demo-grid.mini .dg-card.lit { background: var(--ink); }
.demo-grid.mini .dg-card.dim { opacity: 1; }

/* Screen clip: a recording in a browser frame. */
.screen-clip { border: 1.5px solid var(--surface-edge); border-radius: var(--radius); overflow: hidden; background: var(--surface); box-shadow: var(--lift); }
.screen-clip .sc-bar { height: 44px; display: flex; align-items: center; gap: 18px; padding: 0 16px; background: var(--surface-2); border-bottom: 1px solid var(--surface-edge); }
.screen-clip .sc-dots { width: 52px; height: 12px; background: radial-gradient(circle 6px at 6px 6px, var(--rule) 98%, transparent) 0 0 / 20px 12px repeat-x; }
.screen-clip .sc-address { font: 400 var(--t-min)/1 var(--mono); color: var(--muted); }
.screen-clip video { display: block; width: 100%; height: auto; }

/* Counter and bars. */
.counter { font-variant-numeric: tabular-nums; color: var(--ink); white-space: nowrap; }
.counter.size-display { font: 600 var(--t-display)/1 var(--serif); letter-spacing: -0.02em; }
.counter.size-title { font: 600 var(--t-title)/1 var(--serif); }
.counter.size-lead { font: 600 var(--t-lead)/1 var(--sans); }
.counter.size-body { font: 600 var(--t-body)/1 var(--sans); }
.counter .ct-affix { color: var(--muted); font-weight: 400; }
.bars .bar-row { position: absolute; left: 0; right: 0; }
.bars .bar-label { position: absolute; left: 0; top: 50%; transform: translateY(-50%); font: 400 var(--t-body)/1.15 var(--sans); color: var(--ink); padding-right: 24px; }
.bars .bar-track { position: absolute; top: 12%; bottom: 12%; }
.bars .bar-fill { height: 100%; background: var(--ink-2); border-radius: 0 6px 6px 0; }
.bars .bar-fill.m-proved { background: var(--proved-ink); } .bars .bar-fill.m-tested { background: var(--tested-ink); }
.bars .bar-fill.m-assumed { background: var(--assumed-ink); } .bars .bar-fill.m-spec { background: var(--spec-ink); }
.bars .bar-fill.m-ghost { background: var(--ghost-ink); } .bars .bar-fill.m-unclaimed { background: var(--unclaimed-edge); }
.bars .bar-caption { position: absolute; font: 400 var(--t-min)/1.2 var(--sans); color: var(--muted); }
.bars .bar-val { position: absolute; left: 0; top: 50%; margin-top: -.6em; font: 600 var(--t-body)/1.2 var(--sans); font-variant-numeric: tabular-nums; color: var(--ink); white-space: nowrap; }

/* Camera. */
.camera { position: absolute; overflow: hidden; pointer-events: none; }
.camera > .camera-content { position: absolute; left: 0; top: 0; width: 1920px; height: 1080px; transform-origin: 0 0; pointer-events: auto; }

/* Pointer. */
.pointer { position: absolute; inset: 0; pointer-events: none; }
.pointer-svg { position: absolute; left: 0; top: 0; overflow: visible; }
.pointer-line { fill: none; stroke-width: 2; stroke-linecap: round; stroke: var(--focus-edge); }
.pointer-dot { fill: var(--focus-edge); r: 5.5px; stroke: var(--page); stroke-width: 3px; paint-order: stroke; }
.pointer-label { position: absolute; font: 500 var(--t-body)/1.2 var(--sans); color: var(--ink); background: var(--surface); padding: 6px 18px 7px;
  border-radius: 999px; white-space: nowrap; box-shadow: inset 0 0 0 1.5px var(--focus-edge), var(--lift); }
.pointer-label code { font-size: .88em; }
.pointer-line.m-ghost, .pointer-line.m-spec, .pointer-line.m-proved, .pointer-line.m-rejected, .pointer-line.m-assumed, .pointer-line.m-tested,
.pointer-line.m-unclaimed { stroke: var(--mc-ink); }
.pointer-dot.m-ghost, .pointer-dot.m-spec, .pointer-dot.m-proved, .pointer-dot.m-rejected, .pointer-dot.m-assumed, .pointer-dot.m-tested,
.pointer-dot.m-unclaimed { fill: var(--mc-ink); }
.pointer-label:not(.m-focus) { box-shadow: inset 0 0 0 1.5px var(--mc-edge), var(--lift); }
.m-spec { --mc-ink: var(--spec-ink); --mc-tint: var(--spec-tint); --mc-edge: var(--spec-edge); }
.m-ghost { --mc-ink: var(--ghost-ink); --mc-tint: var(--ghost-tint); --mc-edge: var(--ghost-edge); }
.m-proved { --mc-ink: var(--proved-ink); --mc-tint: var(--proved-tint); --mc-edge: var(--proved-edge); }
.m-tested { --mc-ink: var(--tested-ink); --mc-tint: var(--tested-tint); --mc-edge: var(--tested-edge); }
.m-assumed { --mc-ink: var(--assumed-ink); --mc-tint: var(--assumed-tint); --mc-edge: var(--assumed-edge); }
.m-rejected { --mc-ink: var(--rejected-ink); --mc-tint: var(--rejected-tint); --mc-edge: var(--rejected-edge); }
.m-unclaimed { --mc-ink: var(--unclaimed-ink); --mc-tint: var(--unclaimed-tint); --mc-edge: var(--unclaimed-edge); }
.m-focus { --mc-ink: var(--focus-edge); --mc-tint: var(--focus-tint); --mc-edge: var(--focus-edge); }
.m-obligation { --mc-ink: var(--assumed-ink); --mc-tint: transparent; --mc-edge: var(--assumed-ink); }

/* Subtitles (lib/subtitles.js; its sheet loads after this one, hence the
   two classes). The band is part of the frame's ground: no fill of its
   own, a hairline over the text's width when there are words. */
.subs-layer .subs-band { background: transparent; border-top: 0; }
.subs-layer .subs-band:has(.subs-line)::before { content: ""; position: absolute; top: 0; left: 180px; right: 180px; height: 1px; background: var(--rule); }
.subs-layer .subs-text { color: var(--ink); font-weight: 400; letter-spacing: 0; word-spacing: .02em; }
.subs-layer .subs-word code { color: var(--ink-2); font-weight: 500; }