/* Both themes in one place, `light-dark(light, dark)`, so a colour's two values
   sit together and cannot drift apart. Which one applies is decided by
   `color-scheme`: `light dark` here means "follow the system", and the toggle
   pins it by stamping `data-theme` on the root. That is also what tells the
   browser which way to render the scrollbars and form controls it draws itself.

   The dark values are the original base16 palette. The light ones are the same
   hues darkened until they carry on white -- base16's own light accents are
   mixed for a light *background* but assume a heavier weight than this
   13px monospace, and read as washed out at this size.

   `light-dark()` is required, not progressive: a custom property accepts any
   token sequence, so an older browser stores the call happily and only fails
   later, where `var()` is used -- which means the usual trick of a plain
   declaration ahead of the modern one cannot rescue it. Baseline since 2024
   (Chrome 123, Firefox 120, Safari 17.5). */
:root {
  color-scheme: light dark;
  --bg:     light-dark(#fbfbfb, #181818);
  --fg:     light-dark(#2b2b2b, #d8d8d8);
  --dim:    light-dark(#6b6b6b, #808080);
  --faint:  light-dark(#9b9b9b, #585858);
  --panel:  light-dark(#f2f2f2, #1f1f1f);
  --border: light-dark(#dcdcdc, #383838);
  --hi:     light-dark(#e6ecf5, #2a2f38);
  --sort:   light-dark(#55701a, #a1b56c);
  --term:   light-dark(#26647e, #7cafc2);
  --thm:    light-dark(#834876, #ba8baf);
  --axiom:  light-dark(#9c520f, #dc9656);
  --err:    light-dark(#a5302b, #ab4642);
  --new:    light-dark(#55701a, #a1b56c);
  /* Convertibility gets its own hue. It used to share `--axiom`, which the unify
     view then took for its chrome — leaving conversion commands and the unifier
     the same colour despite being unrelated. Pushed off base16's cyan towards
     green: cyan sits right next to `--term`, which is also the link colour. */
  --conv:   light-dark(#12704a, #7fc9a2);
  /* Variables. Inside an expression the neighbours are term names and
     constants (`--term`, blue) and sort tags (`--dim`), so the two variable
     hues have to separate from those and from each other: base16's green for
     free, its yellow for bound. Warm against cool is the distinction that
     survives being read quickly, which is the one that matters here -- free
     and bound is what the binding conditions turn on.

     `--sort` is the same green and `--axiom` the nearest thing to the yellow;
     neither appears inside an expression. They are kind badges and chrome. */
  --fvar:   light-dark(#55701a, #a1b56c);
  --bvar:   light-dark(#8a6100, #f7ca88);
  /* A warning: something to know about rather than something wrong. `Sorry` is
     the case -- every check passed and the file is still not to be trusted, so
     it is not an error and not nothing. Base16's orange, which `--axiom` also
     uses; they never meet, and naming it for what it means here beats reusing
     a name that means `axiom` somewhere else. */
  --warn:   light-dark(#9c520f, #dc9656);
  /* An informational note: something to know about the file that is neither
     wrong nor a reason to distrust it -- an absent index, no notation table.
     Base16's blue, the coolest tone, so a note never reads as a fault the way
     red or orange would. It is `--term`'s hue; the two never meet, a note being
     chrome and a term name being content. */
  --info:   light-dark(#26647e, #7cafc2);
  /* The selected row, solid rather than a tint: it has to stay legible under
     the marker bars the slots layer on top of it. */
  --cur:    light-dark(#cddcf0, #2d3b4d);
  --ucur:   light-dark(#f4dfc4, #4a3524);
}
/* The toggle pins the scheme; without a stamp the `light dark` above follows
   the system. */
:root[data-theme="light"] { color-scheme: light; }
:root[data-theme="dark"] { color-scheme: dark; }
* { box-sizing: border-box; }
/* The page is a flex column that exactly fills the viewport: the detail view
   must never produce a global scrollbar, or the bottom row gets pushed off
   screen. Each region scrolls internally instead. */
html, body { height: 100%; }
body {
  margin: 0; background: var(--bg); color: var(--fg);
  font: 13px/1.5 ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
  display: flex; flex-direction: column; overflow: hidden;
}
a { color: var(--term); text-decoration: none; }
a:hover { text-decoration: underline; }
/* One line, always. A theorem's crumb carries its full statement, which is
   long; it must give way rather than push the controls onto a second row. */
header {
  /* The right pad matches the vertical one, so the last icon sits the same
     distance from the edge on all three sides it touches. The left keeps its
     wider pad: that side holds text, which needs the margin. */
  padding: 8px 8px 8px 16px; border-bottom: 1px solid var(--border);
  display: flex; align-items: baseline; gap: 12px; flex-wrap: nowrap;
  flex: none;
}
header h1 { font-size: 14px; margin: 0; font-weight: 600; flex: none; }
header h1 a { color: var(--fg); }
header .meta { color: var(--dim); font-size: 12px; }
/* shrinks and truncates instead of wrapping the header */
#crumb {
  flex: 0 1 auto; min-width: 0;
  overflow: hidden; text-overflow: ellipsis; white-space: nowrap;
}
header .spacer { flex: 1 1 0; min-width: 0; }
#nav { flex: none; white-space: nowrap; }
/* The header aligns on baselines, which is right for the title and crumb --
   they read as one line of text. The right-hand group is not text among text
   but labels among 24px controls, and a baseline puts them a pixel above the
   controls' centre line. Centre them with what they sit beside. */
#status, #timing, #nav { align-self: center; }
/* The corner cluster: the controls that belong to the session rather than to
   whatever is on screen.

   All one square, all icons. They were sized by their labels, so a word-wide
   `open…` sat beside a character-wide `?` and the row read as a list of
   unrelated things rather than one set of controls. A fixed box also means
   none of them moves when its glyph or state changes.

   `align-self` because the header is baseline-aligned: a fixed-height box has
   no text baseline of its own to align on, so it would hang low. */
#reload, #help, #proof, #theme {
  flex: none; align-self: center;
  /* 24, matching the step buttons they now sit beside: with the gaps equal,
     a two-pixel difference in height reads as a mistake. */
  width: 24px; height: 24px; padding: 0;
  display: inline-flex; align-items: center; justify-content: center;
  background: var(--panel); color: var(--dim);
  border: 1px solid var(--border); border-radius: 3px;
  font: inherit; line-height: 1; cursor: pointer;
  /* Pulled back against the header's 12px gap to leave 6px, so the controls
     read as one cluster rather than four separate items. The same 6px falls
     between the first of them and the last step button, which is where the
     cluster begins -- an even tighter join there would make the nav look like
     part of it. */
  margin-left: -6px;
}
/* The cluster is a different kind of control from the step buttons beside it,
   so the join keeps a wider gap than the 6px within each group. */
#proof { margin-left: 3px; }
#reload:hover, #help:hover, #proof:hover, #theme:hover {
  background: var(--hi); color: var(--fg);
}
/* The icons are drawn on one grid at one weight, so they need no per-button
   sizing -- which is the point of drawing them rather than setting them. */
#reload svg, #help svg, #proof svg, #theme svg {
  width: 16px; height: 16px; display: block;
  fill: none; stroke: currentColor; stroke-width: 2;
  stroke-linecap: round; stroke-linejoin: round;
}
/* The file-level error: red like every other failure the tool reports -- it
   was orange, which is the colour axioms are drawn in -- and boxed and centred
   rather than run along the top edge, so it reads as a thing that happened
   rather than as another line of chrome. Shaped like `.errbox` below, which
   is the same message at the step level. */
#error {
  color: var(--err); border: 1px solid var(--err);
  background: color-mix(in srgb, var(--err) 13%, transparent);
  border-radius: 3px; padding: 6px 12px; text-align: center;
  margin: 10px auto; width: fit-content; max-width: calc(100% - 32px);
  display: none; flex: none;
}

/* help modal: a fixed backdrop centring a scrollable panel */
.modal { position: fixed; inset: 0; z-index: 50; display: none;
  background: rgba(0, 0, 0, .6); }
.modal.open { display: flex; align-items: center; justify-content: center; }
.modal .box {
  background: var(--panel); border: 1px solid var(--border); border-radius: 6px;
  max-width: 680px; width: calc(100% - 48px); max-height: 82vh; overflow-y: auto;
  padding: 18px 24px 24px; box-shadow: 0 8px 40px rgba(0, 0, 0, .5);
}
.modal .close {
  float: right; background: none; border: none; color: var(--dim);
  font-size: 22px; line-height: 1; cursor: pointer; padding: 0 0 8px 12px;
}
.modal .close:hover { color: var(--fg); }
.modal h2 { margin: 0 0 2px; font-size: 15px; }
.modal h3 { margin: 17px 0 6px; font-size: 11px; color: var(--dim);
  text-transform: uppercase; letter-spacing: .05em; }
.modal p { margin: 6px 0; line-height: 1.55; }
.modal code { color: var(--term); }
.modal kbd {
  display: inline-block; background: var(--bg); border: 1px solid var(--border);
  border-radius: 3px; padding: 0 5px; font: inherit; font-size: 11px;
  color: var(--fg); white-space: nowrap;
}
.modal dl { margin: 6px 0 0; display: grid; grid-template-columns: auto 1fr;
  gap: 5px 16px; align-items: baseline; }
.modal dt { white-space: nowrap; }
.modal dd { margin: 0; color: var(--dim); line-height: 1.4; }
.modal dd.warn { color: var(--warn); }
/* The notes section: advisory, so it sits below the failures rather than among
   them, and reads in the informational hue rather than an alarming one. */
#note-list { margin: 6px 0 0; padding-left: 18px; }
#note-list li { color: var(--info); line-height: 1.5; margin: 3px 0; }
.hidden { display: none; }

/* ---- declaration list ---- */
/* The search box is fixed and the rows scroll under it, rather than the whole
   thing scrolling: filtering is how you reach a declaration among thousands,
   and a control that scrolls away is one you have to scroll back for. A column
   with the box at its natural height and the table taking the rest -- which
   also leaves the header row's `position: sticky` measured against the part
   that actually scrolls. */
#list { flex: 1; min-height: 0; display: flex; flex-direction: column; }
#listbody { flex: 1; min-height: 0; overflow-y: auto; }
#searchrow { flex: none; display: flex; gap: 8px; align-items: stretch; margin: 10px 16px; }
#search {
  flex: 1; min-width: 0;
  padding: 6px 10px;
  background: var(--panel); border: 1px solid var(--border);
  color: var(--fg); border-radius: 4px; font: inherit;
}
/* The failed-only filter. Coloured as a failure rather than as a setting: it
   is the one control whose presence means something is wrong, and the count
   is the point of it. */
#onlybad {
  flex: none; padding: 0 12px; cursor: pointer; white-space: nowrap;
  background: var(--panel); border: 1px solid var(--border);
  border-radius: 4px; font: inherit; color: var(--err);
}
#onlybad:hover { background: var(--hi); }
#onlybad.on { background: var(--err); border-color: var(--err); color: var(--bg); }
#onlybad:empty { display: none; }
table { border-collapse: collapse; width: calc(100% - 32px); margin: 0 16px 24px; table-layout: fixed; }
th, td {
  text-align: left; padding: 3px 8px; border-bottom: 1px solid var(--border);
  overflow: hidden; white-space: nowrap; text-overflow: ellipsis;
}
th {
  color: var(--dim); font-weight: 500;
  position: sticky; top: 0; background: var(--bg);
}
/* ids are s0 / t169 / T2722 — at most 5 chars */
col.c-num { width: 4.5em; } col.c-steps { width: 5em; }
td.num, td.steps { text-align: right; }
td.num { color: var(--faint); } td.steps { color: var(--dim); }
.idtag { color: var(--faint); }
/* The declaration, written as its source writes it and coloured as the step
   page colours it -- one line per row, never wrapped, giving up its parts in
   order when the window is narrow.

   The names inside a *signature* do not take clicks: the row is the target,
   and a link in the middle of it would send you somewhere other than the
   declaration you clicked on. The name itself stays a real link, so it can
   still be copied or opened in a new tab. */
td.decl { white-space: nowrap; }
td.decl .nm, td.decl .sortname { pointer-events: none; }
td.decl .declname { font-weight: 600; }
tbody tr:hover { background: var(--hi); }
tr.hidden { display: none; }
.kind { font-size: 11px; letter-spacing: .3px; }
.k-sort { color: var(--sort); }
.k-term, .k-def, .k-localdef { color: var(--term); }
.k-theorem, .k-pubtheorem { color: var(--thm); }
.k-axiom { color: var(--axiom); }

/* ---- declaration detail ---- */
#detail { display: none; }
#detail.on { display: flex; flex-direction: column; flex: 1; min-height: 0; }
#cols { display: grid; grid-template-columns: 22em 1fr; flex: 1; min-height: 0; }
/* The statement gets its own full-width row, because it is the thing you came
   to read. It lived in the header crumb, where there was no room: it truncated
   — and end-truncation drops the *conclusion*, the most important part. Here it
   wraps, and scrolls if a monster like `grecaux2eqd` needs more than a few lines. */
#stmtbar {
  flex: none; padding: 6px 16px; border-bottom: 1px solid var(--border);
  color: var(--dim); white-space: pre-wrap; word-break: break-word;
  max-height: 5.5em; overflow-y: auto; background: var(--panel);
}
#stmtbar:empty { display: none; }
#stmtbar .declname { color: var(--fg); font-weight: 600; }
#steps {
  overflow-y: auto; border-right: 1px solid var(--border); padding: 4px 0;
}
.step {
  display: flex; gap: 8px; padding: 1px 10px; cursor: pointer; white-space: nowrap;
}
.step:hover { background: var(--hi); }
.step.cur { background: var(--cur); }
/* Marks a step whose command runs the unifier, and steps into it when clicked —
   so it needs a real hit target and to read as a control, not a decoration. */
.step .uflag {
  margin-left: auto; color: var(--axiom); opacity: .45;
  font-size: 11px; flex: none; padding: 0 4px; border-radius: 3px;
  border: 1px solid transparent;
}
.step:hover .uflag, .step.cur .uflag { opacity: 1; }
.step .uflag:hover { border-color: var(--axiom); background: rgba(220, 150, 86, .15); }
/* unify sub-steps, nested under the Thm/Unfold that invokes them */
.step.ustep { padding-left: 26px; background: rgba(220, 150, 86, .05); }
.step.ustep .i { color: var(--axiom); opacity: .6; }
.step.ustep.cur { background: var(--ucur); }
.step .i { color: var(--faint); text-align: right; width: 3.5em; flex: none; }
/* A failed step is marked by its row, not only by its text: the listing is
   scanned, and a colour difference in one word among hundreds of rows is not
   something you find by scanning. Placed after `.step.cur` so that standing on
   the failure still shows it as the failure. */
.step.err, .step.ustep.err {
  color: var(--err); background: color-mix(in srgb, var(--err) 13%, transparent);
}
/* A mark in the margin as well as the shading: the listing is scrolled past at
   speed, a tint can be missed against a shaded row it happens to sit next to,
   and it is the one thing here that carries no shape of its own. Absolutely
   positioned, so no row moves when it appears and none reserves space for it. */
.step { position: relative; }
.step.err::before {
  content: '!'; position: absolute; left: 3px; top: 1px;
  color: var(--err); font-weight: 700;
}
.step.ustep.err::before { left: 14px; }
/* Not a command, so it does not offer to be one: no pointer, no hover. The
   italic is on the text alone -- the `!` is the same mark as on every other
   failed row, and slanting it here would make it a different one. */
.step.norun { cursor: default; }
.step.norun .why { font-style: italic; }
.step.norun:hover { background: color-mix(in srgb, var(--err) 13%, transparent); }
.step.err.cur, .step.ustep.err.cur {
  background: color-mix(in srgb, var(--err) 26%, transparent);
}
.op { color: var(--fg); }
.op-Thm { color: var(--thm); }
.op-Term { color: var(--term); }
/* The `+` joining the two halves of a fused `TermSave`/`ThmSave`. */
.op-fuse { color: var(--faint); }
/* `Sorry` admits its goal: not a failed step, but not a step to pass over. */
.op-Sorry { color: var(--warn); font-weight: bold; }
.op-conv { color: var(--conv); }
/* Stack and heap each own a fixed region that scrolls internally, so neither
   reflows when the other changes size — the whole point of the split. The
   callout sits in its own bottom row of reserved height, so it appearing on a
   `Term`/`Thm` step cannot shove the panes around either. */
#right {
  display: grid;
  grid-template-rows: auto minmax(0, 1fr) minmax(0, 1.5fr) 11em;
  overflow: hidden; min-height: 0;
}
/* Hypotheses are narrow and usually near-empty; the callout wants width for the
   stack effect. Sharing the bottom row uses the horizontal space rather than
   stacking two mostly-empty strips. */
#bottom {
  display: grid; grid-template-columns: minmax(0, 1fr) minmax(0, 2fr);
  min-height: 0; border-top: 1px solid var(--border);
}
#p-hyps { border-right: 1px solid var(--border); border-bottom: none; }
#p-callout { border-bottom: none; min-width: 0; }
/* The unify panes split the stack/heap rows horizontally, and only while the
   unify view is on: by default they are not rendered at all and stack/heap keep
   the full width. The unifier never touches the main heap, but `UHyp` does pop
   proofs off the main stack, so both stay visible beside it. */
.prow { display: grid; grid-template-columns: minmax(0, 1fr); min-height: 0; }
#right.unify .prow { grid-template-columns: minmax(0, 1fr) minmax(0, 1fr); }
.pane.u { display: none; border-left: 1px solid var(--border); }
#right.unify .pane.u { display: flex; }
.pane.u h2 { color: var(--axiom); }

/* A sort has no proof, so it has no machine state: the stack, heap and
   hypotheses would be three empty boxes saying nothing. What a sort *is* is
   its four modifiers, so the callout takes the whole pane and says them. */
#right.sort { grid-template-rows: auto minmax(0, 1fr); }
#right.sort .prow, #right.sort #p-hyps { display: none; }
#right.sort #bottom { grid-template-columns: minmax(0, 1fr); border-top: none; }

/* One line per modifier: the keyword, then what having it means. A modifier
   the sort does not have is struck through rather than omitted -- all four
   apply to every sort, and which ones it lacks is as much of the declaration
   as which ones it has. */
.mods { display: grid; grid-template-columns: auto 1fr; gap: 3px 12px; }
.mods .kw { color: var(--sort); }
.mods .kw.off { color: var(--faint); text-decoration: line-through; }
.mods .gloss { color: var(--dim); }
.mods .gloss.off { color: var(--faint); }
.pane {
  display: flex; flex-direction: column; min-height: 0;
  border-bottom: 1px solid var(--border);
}
.pane h2 {
  font-size: 11px; text-transform: uppercase; letter-spacing: .5px;
  color: var(--dim); margin: 0; font-weight: 500; flex: none;
  padding: 5px 14px 3px; background: var(--bg);
}
.pane .body { overflow-y: auto; min-height: 0; padding: 0 14px 6px; }
#errrow:not(:empty) { padding: 8px 14px 0; }
.slot {
  display: flex; gap: 8px; padding: 1px 0 1px 6px; align-items: baseline;
  border-left: 2px solid transparent;
}
.slot .idx { color: var(--faint); width: 3em; text-align: right; flex: none; }
/* the top of the stack: the end everything pops from */
.slot.top .idx { color: var(--thm); font-weight: bold; }
.slot .val { white-space: pre-wrap; word-break: break-word; }
/* a gutter for the "just pushed" marker, reserved so rows never shift */
.slot .mk { flex: none; width: 1em; color: var(--new); visibility: hidden; }
/* about to be consumed by the active step */
.slot.doomed { border-left-color: var(--err); }
/* pushed by the previous step. Colouring `.val` is useless here: every name is
   inside its own coloured span, so only the parentheses would change. Use a
   marker and a background tint, which read regardless of the contents. */
.slot.fresh { background: rgba(161, 181, 108, .12); }
.slot.fresh .mk { visibility: visible; }
/* The heap slot this `Ref` copies. `outline-offset: -1px` draws the box just
   *inside* the slot: an outline is painted outside the border box, and since we
   scroll this slot into view it ends up flush against the pane's edge, where the
   outside line falls outside the scroll container and is clipped away.
   `scroll-margin` additionally keeps it off the edge when scrolled to. */
.slot.refd {
  outline: 1px solid var(--term); outline-offset: -1px; border-radius: 2px;
  background: rgba(124, 175, 194, .10);
}
.slot { scroll-margin: 3px 0; }
/* In the unifier the cardinality is inverted: a step consumes *one* element and
   pushes *n* (`UTerm` destructures a term into its arguments). So the marker and
   the bar swap roles from the main panes — a ▸ plus a background pick out the
   single consumed element, while a bar spans the pushed group. The group gets no
   background: the bar already delimits it, and tinting n rows is just noise. */
.slot.u-takes { background: rgba(171, 70, 66, .15); }
.slot.u-takes .mk { visibility: visible; color: var(--err); }
.slot.u-makes { border-left-color: var(--new); }
.legend { color: var(--faint); font-size: 11px; margin-left: 8px; font-style: normal; }
.legend .l-utake { color: var(--err); background: rgba(171, 70, 66, .15); padding: 0 3px; }
.legend .l-umake { border-left: 2px solid var(--new); padding-left: 4px; color: var(--new); }
.legend i { font-style: normal; }
.legend .l-doom { border-left: 2px solid var(--err); padding-left: 4px; }
.legend .l-fresh { color: var(--new); background: rgba(161, 181, 108, .12); padding: 0 3px; }
.empty { color: var(--faint); font-style: italic; }
.var { color: var(--fvar); }
.turnstile { color: var(--thm); }
.conv { color: var(--conv); }
/* trailing `: wff` sort annotation — present but not competing with the term */
.sortann { color: var(--dim); }
.errbox {
  color: var(--err); border: 1px solid var(--err); padding: 6px 10px;
  /* Shaded like the rows it is about, so the two read as the same thing. */
  background: color-mix(in srgb, var(--err) 13%, transparent);
  margin-bottom: 12px; display: flex; gap: 10px; align-items: baseline;
}
.errbox .why { flex: 1 1 auto; min-width: 0; }
.errbox button {
  flex: none; font: inherit; cursor: pointer; white-space: nowrap;
  color: var(--err); background: transparent;
  border: 1px solid var(--err); border-radius: 3px; padding: 0 6px;
}
.errbox button:hover { background: var(--err); color: var(--bg); }
/* The callout leads with what went wrong: it is the answer to the question the
   reader is holding, and everything else in the pane describes a step that did
   not finish. */
.po-err { color: var(--err); margin-bottom: 4px; }
/* What the active step does: the declaration it applies, and its stack effect.
   The row has a fixed height and scrolls internally, so stepping across a
   `Ref` -> `Thm` boundary never resizes the panes above. */
.popout { min-width: 0; }
.po-none { color: var(--faint); font-style: italic; }
.po-head { display: flex; gap: 8px; align-items: baseline; }
/* The identity and the signature are one flowing line, so they wrap as one; only
   `po-go` is held out to the right. `min-width: 0` lets it actually shrink. */
.po-decl { min-width: 0; }
.po-go { margin-left: auto; font-size: 11px; color: var(--dim); flex: none; }
.po-u {
  background: var(--panel); color: var(--axiom); border: 1px solid var(--border);
  border-radius: 3px; font: inherit; font-size: 11px; padding: 0 6px;
  cursor: pointer; margin-right: 8px;
}
.po-u:hover { background: var(--hi); }
.po-sig { color: var(--dim); white-space: pre-wrap; word-break: break-word; }
.po-eff { margin-top: 4px; }
.eff { display: flex; gap: 8px; align-items: baseline; padding: 1px 0; }
.eff .lbl {
  flex: none; width: 5.5em; text-align: right; font-size: 11px;
  text-transform: uppercase; letter-spacing: .3px;
}
.eff.takes .lbl { color: var(--err); }
.eff.makes .lbl { color: var(--new); }
.eff .items { min-width: 0; word-break: break-word; }
.eff .sep { color: var(--faint); }
/* schematic names come from the declaration, not the trace */
.schem { color: var(--fg); }
.po-note { color: var(--faint); font-size: 11px; margin-top: 2px; margin-left: 6.5em; }
.nav { display: flex; gap: 6px; align-items: baseline; }
.nav button {
  background: var(--panel); color: var(--fg); border: 1px solid var(--border);
  border-radius: 3px; font: inherit; padding: 1px 8px; cursor: pointer;
}
.nav button:hover { background: var(--hi); }
.nav button:disabled { color: var(--faint); cursor: default; }
kbd {
  color: var(--faint); font-size: 11px;
}
/* Loading indicator: the bar across the top while a file is being read. */
#bar {
  position: fixed; top: 0; left: 0; height: 2px; width: 100%;
  background: linear-gradient(90deg, transparent, var(--term), transparent);
  background-size: 40% 100%; background-repeat: no-repeat;
  animation: slide 1.1s linear infinite; display: none; z-index: 10;
}
#bar.on { display: block; }
@keyframes slide {
  from { background-position: -40% 0 } to { background-position: 140% 0 }
}

/* --- client-side additions ----------------------------------------------
   Everything above dresses the panes themselves. What follows is what only a
   page with no server behind it needs: `.var` takes its own colour because
   variables are drawn in three kinds here, and there is no text spinner,
   because there is nothing to wait on. */

/* The landing state, before a file is open -- which a tool started with a file
   on the command line never has to draw. */
#open {
  flex: 1 1 auto; display: none; flex-direction: column; align-items: center;
  justify-content: center; gap: 18px; padding: 40px; text-align: center;
}
#open.on { display: flex; }
#open h2 { font-weight: 600; font-size: 15px; margin: 0; }
#open p { color: var(--dim); margin: 0; max-width: 46ch; line-height: 1.7; }
#drop {
  border: 1px dashed var(--border); border-radius: 6px; padding: 28px 44px;
  color: var(--dim); background: var(--panel);
}
#drop.over { border-color: var(--term); color: var(--fg); }
#open .examples { display: flex; gap: 10px; flex-wrap: wrap; justify-content: center; }
#open button, #open label {
  background: var(--panel); color: var(--fg); border: 1px solid var(--border);
  border-radius: 3px; font: inherit; padding: 4px 12px; cursor: pointer;
}
#open button:hover, #open label:hover { background: var(--hi); }
#open input[type=file] { display: none; }

/* Verification summary in the header: the whole file's status, which a
   client-side verifier can state and a server-backed viewer could not. */
/* Shrinks *before* the crumb does. The header is one line and the crumb was
   its only flexible item, so adding this pushed the crumb to zero width and
   the declaration you are looking at vanished from the header. On a
   declaration page the crumb is the thing you need; the file's status is
   ambient, so it gives way first. */
#status {
  flex: 0 1000 auto; min-width: 0; font-size: 12px;
  overflow: hidden; text-overflow: ellipsis; white-space: nowrap;
}
#status.ok { color: var(--sort); }
#status.bad { color: var(--err); cursor: pointer; }
#status.warn { color: var(--warn); cursor: pointer; }
#status.bad:hover, #status.warn:hover { text-decoration: underline; }
#status.busy { color: var(--dim); }
/* A verified file can still carry notes; the ✓ stays green -- verification did
   pass -- but the badge becomes a way into the modal, so it takes the pointer
   and hover the failing badges have. `.compact` otherwise pins the cursor to
   default, so this has to win over it. */
#status.notes, #status.compact.notes { cursor: pointer; }
#status.notes:hover { text-decoration: underline; }

/* The list and the detail view are alternatives; the detail view already had
   an `.on` class, so the list gets the matching `.off`. Toggling classes
   rather than inline styles keeps the display rules in one place. */
#list.off { display: none; }

/* Statement and signature parts. The statement row is dim as a whole -- it is
   reference, not the thing you are stepping -- so the pieces that carry meaning
   are lifted back out of it rather than the row being brightened. Variables use
   the extracted block's own `.var`, which said exactly this already. */
/* The `$` fences delimit a formula; they are structure, and subdued so the
   formula reads over them. */
.fence { color: var(--faint); }
/* `{ } ( ) : >` -- the syntax around the formulas, which you do read. */
.punct { color: var(--fg); }
/* A sort is a declaration, so it links; dim because a binder's sort is
   context rather than content. */
/* On the class, not the anchor: a sort with nowhere to link is drawn as a span
   and still has to look like a sort. Only the link responds to hovering. */
.sortname { color: var(--dim); }
a.sortname:hover { color: var(--fg); }
/* A declaration's name, whether or not it can be followed. Only anchors were
   coloured -- by the bare `a` rule, not by this class -- so a name the file
   cannot resolve, which is exactly the case worth noticing, was the one
   rendered as ordinary text. */
.nm { color: var(--term); }

/* Something the file names that is not there: an id past the end of a table, or
   an argument a malformed expression never supplied. Boxed rather than merely
   recoloured -- drawn as an ordinary name it reads as one that happens to be
   spelled `s48`, which is the reading that hides the defect.

   Not `.err`: that says a *row* failed, and a rule written for a token was
   matching `.step.err` too -- giving every failed step a border and 2px of
   padding where it should have had 10, so it sat out of line with the rest of
   the listing. Two meanings, two names. */
.missing {
  color: var(--err); border: 1px solid var(--err);
  border-radius: 2px; padding: 0 2px;
}

/* The three kinds of variable, each drawn as itself. A free one had been left
   in the foreground colour on the argument that it is the commonest case and
   colouring it would tint most of every expression -- but that made a variable
   indistinguishable from ordinary text, which is the thing this is for.

   A dummy is a bound variable that nothing outside can name: a narrowing of
   the same idea rather than a different one, so it is the same colour set in
   italic. A third hue would say the two were unrelated. */
.bvar { color: var(--bvar); }
.dummy { font-style: italic; }
/* A declaration that failed to verify is the row worth finding, so it is
   marked in the list rather than only in the error line. */
#decls tr.bad .declname { color: var(--err); }
#decls tr.bad { background: color-mix(in srgb, var(--err) 8%, transparent); }

/* The proof-only toggle. A turnstile because that is the glyph the panes use
   to mark a proof, which is what the filter keeps; and because the header is
   one line, on which the crumb is the only item that can give way.

   It lives with the other controls in the corner rather than inside `#nav`:
   `#nav` is rebuilt per step and emptied on the list, so the filter moved and
   then vanished depending on where you were, even though it is a setting that
   applies throughout. Its width does not change with its state -- the count is
   in the tooltip -- so toggling never shifts the row. */
/* Filled, not merely recoloured. This is an icon-only toggle at 24px, and a
   thin stroke changing hue is not a state you can read at a glance -- a filled
   box is, and it is what a checked control looks like.

   The id is load-bearing: `.tog.on` is two classes and lost to every `#proof`
   rule in the cluster above, so the active state was not being drawn at all.
   `:hover` is matched too, or pointing at the control while it is on would
   paint the off state back over it. */
#proof.on, #proof.on:hover {
  background: var(--thm); border-color: var(--thm); color: var(--bg);
}


/* The keyboard hint duplicates the help modal, which is one keypress away, so
   it is the first thing to go when the row is tight -- 232px of reminder is a
   poor trade against the name of the declaration you are reading. */
@media (max-width: 1500px) { #nav kbd { display: none; } }

/* The compact status is a badge, not a bare glyph. `✓` in the body's monospace
   face renders small and thin -- it is sized for a text column, not to be read
   at a glance -- so it gets a UI face at full weight inside a ring, which also
   gives the mark an outline to carry its colour. */
#status.compact {
  flex: none; align-self: center;
  display: inline-flex; align-items: center; justify-content: center;
  width: 17px; height: 17px; border-radius: 50%;
  border: 1.5px solid currentColor;
  font: 600 11px/1 system-ui, -apple-system, Segoe UI, sans-serif;
  cursor: default;
}
/* The warning sign is a triangle, which carries its own outline -- a ring
   round it would be an outline round an outline. */
#status.compact.warn { border: none; font-size: 15px; }

/* The verification time, beside the badge. The claim being made is that this
   is fast, so it is stated rather than left in a tooltip. */
/* The count of failures, beside the badge that says there were some. Shaped
   like the error boxes it replaced -- a summary of the same thing, in the one
   place that is on screen whatever you are looking at -- but set shorter than
   the controls beside it so the header keeps its height. */
#failures {
  flex: none; align-self: center; font: inherit; font-size: 12px; cursor: pointer;
  padding: 0 7px; line-height: 18px; border-radius: 3px; white-space: nowrap;
  color: var(--err); border: 1px solid var(--err);
  background: color-mix(in srgb, var(--err) 13%, transparent);
}
#failures:hover { background: var(--err); color: var(--bg); }
/* Nothing failed, so the count is a warning rather than a verdict. */
#failures.warn {
  color: var(--warn); border-color: var(--warn);
  background: color-mix(in srgb, var(--warn) 13%, transparent);
}
#failures.warn:hover { background: var(--warn); color: var(--bg); }
/* Nothing failed and nothing used sorry: the count is purely informational. */
#failures.info {
  color: var(--info); border-color: var(--info);
  background: color-mix(in srgb, var(--info) 13%, transparent);
}
#failures.info:hover { background: var(--info); color: var(--bg); }
#failures:empty { display: none; }
#timing { flex: none; color: var(--sort); font-size: 12px; }
/* How long it took is not a good-news item when the answer was no. */
#timing.bad { color: var(--err); }
#timing.warn { color: var(--warn); }
#timing:empty { display: none; }