/* ===========================================================================
   Aether -- typeset like a proof, not built like a dashboard.

   Three ideas hold this together.

   1. One palette, in the --wa-* token layer.  Web Awesome's stylesheet defines
      every colour as a custom property inside cascade layers; this file is
      unlayered, and unlayered CSS outranks layered CSS, so everything below
      both overrides those defaults and stays the single source of truth.  The
      app's own names are aliases of the --wa-* semantics rather than a second,
      parallel set of hex values.

   2. Monospace everywhere except the intern's prose.  The formal layer -- the
      proof itself, the line numbers, the variables, the hypotheses, the
      verdict -- is machine-checked, so it is set in JetBrains Mono.  The only
      things that break the grid are the sentences where the checker explains
      itself in English.  That split is the whole type system; there is no
      second family.

   3. Failure is the event.  A valid step is the unremarkable case, so it gets
      no box, no fill and no colour.  A step that fails gets a rail in the
      margin, and so does everything after it, because everything after it
      rests on it.

   Component internals live in shadow DOM and cannot be reached from here at
   all.  Density is expressed through the token layer (the scale knobs below)
   and through ::part() where a component exposes one -- never by trying to
   restyle internals.
   =========================================================================== */

:root {
  color-scheme: light;

  /* --- Density and geometry ---------------------------------------------
     Each knob scales a whole family of component tokens at once.  The radii
     are deliberately near-square: an instrument, not a web page. */
  --wa-font-size-scale: 0.8125; /* 16px -> 13px base */
  --wa-space-scale: 0.7;
  --wa-border-radius-scale: 0.3;
  --wa-line-height-normal: 1.45;
  --wa-focus-ring-width: 0.125rem;
  --wa-focus-ring-offset: 0.0625rem;

  /* No drop shadows anywhere: a floating layer is separated by its surface
     and a hairline, so the components' own elevation is switched off. */
  --wa-shadow-s: none;
  --wa-shadow-m: none;
  --wa-shadow-l: none;

  --wa-font-family-body: var(--font-mono);
  --wa-font-family-code: var(--font-mono);

  /* --- Palette: light --------------------------------------------------- */
  --wa-color-surface-default: #ffffff;
  --wa-color-surface-raised: #f7f8f9;
  --wa-color-surface-lowered: #eff1f4;
  --wa-color-surface-border: #dde1e6;

  --wa-color-text-normal: #16181d;
  --wa-color-text-quiet: #555b6a;
  /* The quietest text that is still text: line numbers, path, "VALID".
     Both quiet steps clear 4.5:1 on every surface they sit on. */
  --app-text-dim: #666c7a;
  --wa-color-text-link: #0a5fbf;

  --wa-color-focus: #0a5fbf;
  --wa-color-overlay-modal: rgba(22, 24, 29, 0.42);

  --wa-color-brand-fill-loud: #0a5fbf;
  --wa-color-brand-on-loud: #ffffff;
  --wa-color-brand-fill-quiet: rgba(10, 95, 191, 0.08);
  --wa-color-brand-on-quiet: #0a5fbf;

  --wa-color-success-fill-quiet: rgba(21, 115, 51, 0.09);
  --wa-color-success-on-quiet: #157333;
  --wa-color-success-fill-loud: #157333;

  --wa-color-warning-fill-quiet: rgba(125, 78, 0, 0.1);
  --wa-color-warning-on-quiet: #7d4e00;
  --wa-color-warning-fill-loud: #7d4e00;

  --wa-color-danger-fill-quiet: rgba(190, 24, 36, 0.08);
  --wa-color-danger-on-quiet: #be1824;
  --wa-color-danger-fill-loud: #be1824;

  --wa-color-neutral-fill-quiet: rgba(22, 24, 29, 0.05);
  --wa-color-neutral-on-quiet: #555b6a;
  --wa-color-neutral-border-normal: #dde1e6;
  /* A secondary button sits on lowered paper, not a chip. */
  --wa-color-neutral-fill-normal: #eff1f4;
  --wa-color-neutral-on-normal: #16181d;
  /* One boundary for every form control, native or Web Awesome, at 3:1 on paper. */
  --app-control-border: #8a909c;
  --wa-form-control-border-color: var(--app-control-border);
}

[data-theme="dark"] {
  color-scheme: dark;

  --wa-color-surface-default: #0e1013;
  --wa-color-surface-raised: #15181c;
  --wa-color-surface-lowered: #1a1e23;
  --wa-color-surface-border: #262b32;

  --wa-color-text-normal: #e6e8ec;
  --wa-color-text-quiet: #9ba3b0;
  --app-text-dim: #7f8795;
  --wa-color-text-link: #6cb0ff;

  --wa-color-focus: #6cb0ff;
  --wa-color-overlay-modal: rgba(0, 0, 0, 0.62);

  --wa-color-brand-fill-loud: #1f6feb;
  --wa-color-brand-on-loud: #ffffff;
  --wa-color-brand-fill-quiet: rgba(108, 176, 255, 0.1);
  --wa-color-brand-on-quiet: #6cb0ff;

  --wa-color-success-fill-quiet: rgba(74, 185, 96, 0.11);
  --wa-color-success-on-quiet: #4ab960;
  --wa-color-success-fill-loud: #238636;

  --wa-color-warning-fill-quiet: rgba(214, 160, 31, 0.13);
  --wa-color-warning-on-quiet: #d9a520;
  --wa-color-warning-fill-loud: #9e6a03;

  --wa-color-danger-fill-quiet: rgba(242, 100, 92, 0.11);
  --wa-color-danger-on-quiet: #f2645c;
  --wa-color-danger-fill-loud: #da3633;

  --wa-color-neutral-fill-quiet: rgba(230, 232, 236, 0.06);
  --wa-color-neutral-on-quiet: #9ba3b0;
  --wa-color-neutral-border-normal: #262b32;
  --wa-color-neutral-fill-normal: #1a1e23;
  --wa-color-neutral-on-normal: #e6e8ec;
  --app-control-border: #646b77;
  --wa-form-control-border-color: var(--app-control-border);
}

/* --- Syntax: the vivid scheme ----------------------------------------------
   Opted into from the tool strip (see js/editor.js and aether-language.js).  Same
   token vocabulary as above, different values: each *category* of word gets
   its own hue, the way a general-purpose language colours strings, calls and
   keywords apart.  Chosen to survive on a white page first; the dark block
   below re-picks every one of them for a near-black one.

   Glue words (such, that, from, by) and comments stay quiet in both schemes --
   they are connective tissue, and colouring them would bury the real
   structure. */
:root[data-syntax="vivid"] {
  --cm-token-structure: #6d28d9; /* Theorem, Proof, QED, Case */
  --cm-token-intro: #0a5fbf; /* Let, Given, Assume, Obtain, Step */
  --cm-token-flow: #0d7a6b; /* Therefore, Hence, exists, forall */
  --cm-token-join: #5f6672; /* such, that, from, by -- quiet */
  --cm-token-logic: #c2410c; /* and, or, not, in, mod */
  --cm-token-math-fn: #4338ca; /* sqrt, det, lim, integrate */
  --cm-token-macro: #0e7490; /* \\mathbb{N}, \\epsilon */
  --cm-token-type: #b02a7a; /* Int, Real, Even, MultipleOf */
  --cm-token-ink: #16181d; /* names and binders */
  --cm-token-number: #b45309;
  --cm-token-operator: #4b5563;
  --cm-token-string: #0a7a4a;
  --cm-token-comment: #666c7a; /* quiet */
}

:root[data-theme="dark"][data-syntax="vivid"] {
  --cm-token-structure: #c4a7ff;
  --cm-token-intro: #7cb7ff;
  --cm-token-flow: #5fd3be;
  --cm-token-join: #8b929c;
  --cm-token-logic: #ffa678;
  --cm-token-math-fn: #a5b4ff;
  --cm-token-macro: #67d6e8;
  --cm-token-type: #f9a8d4;
  --cm-token-ink: #e6e8ec;
  --cm-token-number: #f5c97b;
  --cm-token-operator: #9aa1ac;
  --cm-token-string: #7bd98f;
  --cm-token-comment: #7f8795;
}

/* --- Type and the app's own vocabulary ------------------------------------ */
:root {
  /* The formal layer.  See fonts.css for the subsets and ui/vendor_fonts.py for
     where they come from. */
  --font-mono: "JetBrains Mono", ui-monospace, SFMono-Regular, "SF Mono", Menlo,
    Consolas, monospace;
  /* The intern's voice.  Only ever used for sentences. */
  --font-prose: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica,
    Arial, sans-serif;

  --bg: var(--wa-color-surface-default);
  --panel: var(--wa-color-surface-raised);
  --panel-2: var(--wa-color-surface-lowered);
  --panel-3: color-mix(in oklab, var(--wa-color-text-normal) 6%, var(--wa-color-surface-default));
  --border: var(--wa-color-surface-border);
  /* The 1px structure lines.  Barely there on purpose: they organise the page
     without drawing boxes around anything. */
  --hairline: color-mix(in oklab, var(--wa-color-text-normal) 8%, var(--wa-color-surface-default));
  --text: var(--wa-color-text-normal);
  --muted: var(--wa-color-text-quiet);
  --muted-dim: var(--app-text-dim);

  --valid: var(--wa-color-success-on-quiet);
  --valid-bg: var(--wa-color-success-fill-quiet);
  --warning: var(--wa-color-warning-on-quiet);
  --warning-bg: var(--wa-color-warning-fill-quiet);
  --invalid: var(--wa-color-danger-on-quiet);
  --invalid-bg: var(--wa-color-danger-fill-quiet);
  --accent: var(--wa-color-text-link);
  --accent-bg: var(--wa-color-brand-fill-quiet);

  --danger-text: var(--wa-color-danger-on-quiet);
  --note-cex-text: var(--wa-color-danger-on-quiet);
  --note-dom-text: var(--wa-color-warning-on-quiet);
  --selected-ring: color-mix(in oklab, var(--wa-color-text-normal) 22%, transparent);

  --radius: 2px;
  --radius-sm: 2px;

  /* Editor surface.  CodeMirror cannot read custom properties itself, so
     editor.js resolves these with getComputedStyle: that keeps the palette
     single-source instead of duplicated as literals in JavaScript. */
  --cm-bg: var(--wa-color-surface-default);
  --cm-text: var(--wa-color-text-normal);
  --cm-caret: var(--accent);
  --cm-gutter-fg: var(--muted-dim);
  --cm-gutter-border: color-mix(in oklab, var(--wa-color-text-normal) 8%, var(--wa-color-surface-default));
  --cm-gutter-active-fg: var(--muted);
  --cm-gutter-active-bg: color-mix(in oklab, var(--wa-color-text-normal) 4%, var(--wa-color-surface-default));
  --cm-active-line: color-mix(in oklab, var(--wa-color-text-normal) 3%, var(--wa-color-surface-default));
  --cm-selection: color-mix(in oklab, var(--accent) 20%, transparent);
  --cm-selection-focused: color-mix(in oklab, var(--accent) 32%, transparent);
  --cm-placeholder: var(--app-text-dim);
  --cm-tooltip-bg: var(--wa-color-surface-raised);
  --cm-tooltip-border: var(--wa-color-surface-border);

  /* Syntax -- the "mono" scheme, which is the default.

     Nearly monochrome by design: the CNL keywords are the skeleton of the
     proof and take the accent, types are inked and separated by weight, and
     operators, glue words, strings and comments recede.  The result reads as
     text with a structure rather than as a rainbow.

     Every token is its own variable because the "vivid" scheme below needs to
     colour the categories apart; here they simply share values.  These are
     aliases of the palette rather than literals, so they follow the dark theme
     with no second definition -- only the vivid scheme needs both, since its
     hues are chosen for contrast against one background apiece. */
  --cm-token-structure: var(--accent);
  --cm-token-intro: var(--accent);
  --cm-token-flow: var(--accent);
  --cm-token-join: var(--muted-dim);
  --cm-token-logic: var(--accent);
  --cm-token-math-fn: var(--accent);
  --cm-token-macro: var(--text);
  --cm-token-type: var(--text);
  --cm-token-ink: var(--text);
  --cm-token-number: var(--text);
  --cm-token-operator: var(--muted);
  --cm-token-string: var(--muted);
  --cm-token-comment: var(--muted-dim);
}

* {
  box-sizing: border-box;
}

html,
body {
  height: 100%;
  margin: 0;
}

body {
  background: var(--bg);
  color: var(--text);
  font-family: var(--font-mono);
  font-size: 13px;
  line-height: 1.5;
  /* The app grid: the rail and the current view side by side, the status bar
     across the foot.  Only one view is ever in the grid at a time. */
  display: grid;
  grid-template-columns: 44px minmax(0, 1fr);
  grid-template-rows: minmax(0, 1fr) 24px;
  grid-template-areas: "rail view" "status status";
  overflow: hidden;
  -webkit-font-smoothing: antialiased;
}

.sr-only {
  position: absolute;
  width: 1px;
  height: 1px;
  padding: 0;
  margin: -1px;
  overflow: hidden;
  clip: rect(0, 0, 0, 0);
  white-space: nowrap;
  border: 0;
}

/* The one place the grid is deliberately broken: prose. */
.step-message,
.ctx-empty,
.empty-state {
  font-family: var(--font-prose);
}

/* =========================================================================
   Web Awesome host shims
   Component internals are unreachable, but the host element and any exported
   part belong to us.
   ========================================================================= */

/* Icons are inlined SVGs, not <wa-icon>.
   A slotted <svg> inside <wa-icon> is never painted: the component's shadow root
   is a single empty <svg part="svg"> with no <slot>, because it only renders
   from `name`/`src` -- so every icon here sat at 0x0 and rendered nothing.  A
   plain <svg> inside <wa-button> lands in the button's own label slot instead.
   The size is in `em` so the icon follows the button's font-size.
   (A `name` icon is not an option anyway: it fetches from ka-f.fontawesome.com
   at runtime, and this app makes no cross-origin requests.) */
.icon {
  display: block;
  flex: none;
  width: 1em;
  height: 1em;
}

/* Show the theme you would switch *to*. */
[data-theme="light"] .icon--sun,
[data-theme="dark"] .icon--moon {
  display: none;
}

/* Same idea for syntax colours: the icon shows the scheme you would switch
   *to*, so one filled dot reads "click for a single hue" and three read
   "click for colour". */
[data-syntax="mono"] .icon--vivid,
[data-syntax="vivid"] .icon--mono {
  display: none;
}

/* Every switch, reduced to an ink toggle.  Off and on differ by ink, not by
   hue: a stock filled pill is the loudest object on an otherwise hairlined
   page, and the switches here decide how a proof is judged and exported, so
   none of them should compete with the verdict they produce. */
wa-switch {
  --height: 14px;
  --width: 26px;
  --thumb-size: 8px;
  --wa-form-control-activated-color: var(--text);
  --wa-form-control-label-color: var(--text);
}

wa-switch::part(control) {
  background: var(--panel-2);
  border: 1px solid var(--hairline);
  border-radius: var(--radius-sm);
}

wa-switch::part(thumb) {
  background: var(--muted-dim);
  border-color: transparent;
  border-radius: 1px;
}

wa-switch:state(checked)::part(control) {
  background: var(--text);
  border-color: var(--text);
}

wa-switch:state(checked)::part(thumb) {
  background: var(--bg);
}

/* A tighter label than the dialog switches need, since this one sits in the
   tool strip above the proof. */
.strict-switch {
  flex: none;
  font-size: 12px;
  margin-left: 4px;
}

.strict-switch::part(label) {
  font-size: 12px;
  font-weight: 600;
  white-space: nowrap;
}

.strict-switch::part(hint) {
  font-size: 11px;
  color: var(--muted-dim);
}

wa-spinner {
  width: 10px;
  height: 10px;
  font-size: 11px;
  vertical-align: -1px;
}

.verdict-block {
  display: flex;
  align-items: baseline;
  gap: 10px;
  min-width: 0;
}

/* A rail and a word, in the same language as the auditor's margin.  The
   rail carries the status, so the palette stays quiet: green appears here and
   nowhere else, which is what lets red land when it does. */
.verdict {
  font-family: var(--font-mono);
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 1px;
  text-transform: uppercase;
  padding: 2px 0 2px 8px;
  border-left: 2px solid var(--muted-dim);
  white-space: nowrap;
}

.verdict--idle {
  color: var(--muted);
  border-left-color: var(--border);
}

.verdict--valid {
  color: var(--valid);
  border-left-color: var(--valid);
}

.verdict--warning {
  color: var(--warning);
  border-left-color: var(--warning);
}

.verdict--invalid,
.verdict--parse-error {
  color: var(--invalid);
  border-left-color: var(--invalid);
}

.verdict--pending {
  color: var(--accent);
  border-left-color: var(--accent);
}

/* An edit has landed and the debounced re-check has not answered yet, so the
   verdict on screen describes the previous buffer. */
.verdict.is-stale {
  opacity: 0.45;
}

.verdict-meta {
  font-size: 11px;
  color: var(--muted-dim);
  font-variant-numeric: tabular-nums;
  white-space: nowrap;
  min-width: 0;
  overflow: hidden;
  text-overflow: ellipsis;
}

/* =========================================================================
   Layout
   ========================================================================= */

/* The grid.  Placement is by *slot name*, not by DOM order: js/layout.js
   stamps data-slot="a|b|c" on the three panes in whatever order the user has
   them, and each arrangement below says where those three slots sit.  Swapping
   two panels is therefore a swap of two slot names, so no arrangement rule has
   to know which panel is which, and every arrangement stays meaningful after
   any swap. */
.layout {
  flex: 1 1 auto;
  min-height: 0;
  display: grid;
  gap: 1px;
  background: var(--border);
}

.layout[data-layout="columns"],
.layout:not([data-layout]) {
  grid-template-columns: minmax(0, 1.1fr) minmax(0, 1fr) minmax(0, 0.85fr);
  grid-template-areas: "a b c";
}

/* Three panels in one column: reading rather than comparing. */
.layout[data-layout="stack"] {
  grid-template-columns: minmax(0, 1fr);
  grid-template-rows: minmax(0, 1.15fr) minmax(0, 1fr) minmax(0, 0.9fr);
  grid-template-areas: "a" "b" "c";
}

/* Editor above; the auditor and the context pair up beneath it. */
.layout[data-layout="split"] {
  grid-template-columns: minmax(0, 1fr) minmax(0, 1fr);
  grid-template-rows: minmax(0, 1.75fr) minmax(0, 1fr);
  grid-template-areas: "a a" "b c";
}

/* Editor beside the pair, which stack in the second column -- the closest
   thing to docking one panel inside another. */
.layout[data-layout="focus"] {
  grid-template-columns: minmax(0, 1.4fr) minmax(0, 1fr);
  grid-template-rows: minmax(0, 1fr) minmax(0, 1fr);
  grid-template-areas: "a b" "a c";
}

.pane[data-slot="a"] {
  grid-area: a;
}

.pane[data-slot="b"] {
  grid-area: b;
}

.pane[data-slot="c"] {
  grid-area: c;
}

/* While a panel is being dragged, the one under the pointer is outlined. */
.pane[data-drop-target] {
  outline: 2px solid var(--accent);
  outline-offset: -2px;
}

.pane[data-dragging] {
  opacity: 0.55;
}

.pane {
  background: var(--bg);
  display: flex;
  flex-direction: column;
  min-height: 0;
  min-width: 0;
}

/* Flat.  The head is a label and a rule, with no fill of its own, so the only
   strong horizontal line in a pane is the one under its title. */
.pane-head {
  display: flex;
  align-items: center;
  gap: 10px;
  padding: 5px 12px;
  border-bottom: 1px solid var(--border);
  flex: 0 0 auto;
  min-height: 30px;
}

.pane-head h2 {
  margin: 0;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
  white-space: nowrap;
}

.pane-note {
  margin: 0 0 0 auto;
  font-size: 11px;
  color: var(--muted-dim);
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}

.pane-tools {
  margin-left: auto;
  display: flex;
  align-items: center;
  gap: 3px;
}

.scroll {
  overflow: auto;
  min-height: 0;
  flex: 1 1 auto;
}

kbd {
  font-family: var(--font-mono);
  font-size: 11px;
  line-height: 1;
  padding: 1px 3px;
  border: 1px solid var(--border);
  border-bottom-width: 2px;
  border-radius: 2px;
  background: var(--panel-3);
  color: var(--muted);
}

.blurb {
  margin: 0;
  padding: 5px 12px;
  font-size: 11px;
  color: var(--muted);
  border-bottom: 1px solid var(--hairline);
  flex: 0 0 auto;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}

.blurb strong {
  color: var(--text);
  font-weight: 600;
}

/* =========================================================================
   Editor
   ========================================================================= */

.editor {
  flex: 1 1 auto;
  min-height: 0;
  overflow: hidden;
}

.editor .cm-editor {
  height: 100%;
}

.editor .cm-editor.cm-focused {
  outline: none;
}

/* =========================================================================
   Auditor

   No cards.  Each row is a line number in the margin, the statement, and its
   status set as type on the right; the only rules are hairlines, and the only
   rails belong to steps that failed -- or that rest on one that did.
   ========================================================================= */

.audit {
  padding: 0;
}

.report-group {
  margin: 0;
}

.report-header {
  display: flex;
  align-items: baseline;
  gap: 8px;
  padding: 9px 12px 6px;
  font-size: 11px;
  color: var(--muted-dim);
  border-bottom: 1px solid var(--hairline);
}

.report-header .report-name {
  color: var(--text);
  font-weight: 600;
}

.report-verdict {
  margin-left: auto;
  font-size: 11px;
  letter-spacing: 0.8px;
  text-transform: uppercase;
  color: var(--muted-dim);
}

.step {
  position: relative;
  display: grid;
  grid-template-columns: 22px minmax(0, 1fr);
  gap: 11px;
  width: 100%;
  text-align: left;
  font: inherit;
  color: inherit;
  cursor: pointer;
  background: none;
  border: 0;
  border-bottom: 1px solid var(--hairline);
  border-radius: 0;
  padding: 8px 12px 8px 14px;
  transition: background 0.1s ease;
}

/* The entailment rule.  Rows are flush, so consecutive rails read as one
   continuous line down the margin. */
.step::before {
  content: "";
  position: absolute;
  top: 0;
  bottom: 0;
  left: 0;
  width: 2px;
  background: transparent;
}

.step--warning::before {
  background: var(--warning);
}

.step--invalid::before {
  background: var(--invalid);
}

/* Everything below the break is suspect: it was justified by a step that did
   not hold.  Still marked, but quieter than the break itself. */
.step.is-downstream::before {
  background: color-mix(in oklab, var(--invalid) 30%, transparent);
}

.step:hover {
  background: var(--panel-2);
}

.step:focus-visible {
  outline: 2px solid var(--accent);
  outline-offset: -2px;
}

/* Selection is a ring, not a fill or a rail, so it can never be confused with
   a status -- and never covers one up. */
.step.is-selected {
  background: var(--panel-2);
  box-shadow: inset 0 0 0 1px var(--selected-ring);
}

.step-line {
  font-size: 11px;
  color: var(--muted-dim);
  text-align: right;
  font-variant-numeric: tabular-nums;
  padding-top: 1px;
}

.step-body {
  min-width: 0;
}

.step-head {
  display: flex;
  align-items: baseline;
  gap: 12px;
}

.step-statement {
  flex: 1 1 auto;
  min-width: 0;
  font-family: var(--font-mono);
  font-size: 13px;
  line-height: 1.45;
  color: var(--text);
  word-break: break-word;
  white-space: pre-wrap;
}

.step-meta {
  flex: 0 0 auto;
  display: flex;
  align-items: baseline;
  gap: 5px;
  font-size: 11px;
  letter-spacing: 0.4px;
  white-space: nowrap;
}

.status {
  text-transform: uppercase;
  letter-spacing: 0.7px;
}

/* A step that held is not news. */
.status--valid {
  color: var(--muted-dim);
  font-weight: 400;
}

.status--warning {
  color: var(--warning);
  font-weight: 700;
}

.status--invalid {
  color: var(--invalid);
  font-weight: 700;
}

.meta-sep {
  color: var(--muted-dim);
  opacity: 0.45;
}

.backend,
.depth {
  color: var(--muted-dim);
}

.step-message {
  margin: 4px 0 0;
  font-size: 12px;
  line-height: 1.5;
  color: var(--muted);
  word-break: break-word;
}

.note {
  margin: 6px 0 0;
  font-size: 11px;
  line-height: 1.45;
  border-radius: var(--radius-sm);
  padding: 5px 8px;
  word-break: break-word;
}

.note--counterexample {
  color: var(--note-cex-text);
  background: var(--invalid-bg);
  border-left: 2px solid var(--invalid);
}

.note--domain {
  color: var(--note-dom-text);
  background: var(--warning-bg);
  border-left: 2px solid var(--warning);
}

.note-label {
  font-weight: 700;
  letter-spacing: 0.9px;
  text-transform: uppercase;
  font-size: 11px;
  display: block;
  margin-bottom: 2px;
}

/* =========================================================================
   Context
   ========================================================================= */

.context {
  padding: 10px 12px;
}

.ctx-empty {
  color: var(--muted-dim);
  font-size: 12px;
  line-height: 1.55;
}

.ctx-title {
  font-size: 12px;
  color: var(--text);
  margin: 0 0 9px;
  word-break: break-word;
  line-height: 1.45;
}

.ctx-section {
  margin-bottom: 13px;
}

.ctx-section h3 {
  margin: 0 0 6px;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 1px;
  text-transform: uppercase;
  color: var(--muted-dim);
}

.chips {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
}

.chip {
  font-size: 11px;
  padding: 2px 6px;
  border-radius: var(--radius-sm);
  border: 1px solid var(--border);
  color: var(--text);
}

.chip-name {
  color: var(--accent);
}

.chip-type {
  color: var(--muted);
}

.ctx-list {
  list-style: none;
  margin: 0;
  padding: 0;
  display: flex;
  flex-direction: column;
  gap: 2px;
}

.ctx-list li {
  font-size: 11px;
  line-height: 1.5;
  padding: 3px 7px;
  border-radius: var(--radius-sm);
  border-left: 2px solid var(--hairline);
  background: var(--panel-2);
  word-break: break-word;
}

/* Not italic: the vendored subsets ship no italic file, and a synthesised
   slant on a monospace face looks like a rendering fault. */
.ctx-none {
  font-size: 12px;
  color: var(--muted-dim);
}

.ctx-facts {
  display: grid;
  grid-template-columns: auto 1fr;
  gap: 2px 10px;
  font-size: 11px;
  margin-bottom: 12px;
}

.ctx-facts dt {
  color: var(--muted-dim);
}

.ctx-facts dd {
  margin: 0;
  color: var(--text);
}

/* =========================================================================
   Parse error / empty state
   ========================================================================= */

.parse-error {
  border-left: 2px solid var(--invalid);
  background: var(--invalid-bg);
  padding: 10px 12px;
}

.parse-error h3 {
  margin: 0 0 5px;
  font-size: 11px;
  letter-spacing: 1px;
  text-transform: uppercase;
  color: var(--invalid);
}

.parse-error .location {
  font-size: 12px;
  color: var(--danger-text);
  margin-bottom: 7px;
}

.parse-error pre {
  margin: 0;
  font-family: var(--font-mono);
  font-size: 11px;
  line-height: 1.5;
  color: var(--muted);
  white-space: pre-wrap;
  word-break: break-word;
  max-height: 240px;
  overflow: auto;
}

.empty-state {
  color: var(--muted-dim);
  font-size: 12px;
  padding: 12px;
  line-height: 1.55;
}

/* =========================================================================
   History (a panel of the reading pane)
   ========================================================================= */

.pane--editor {
  position: relative;
}

#history-panel {
  padding: 12px;
}

.history-head {
  display: flex;
  align-items: center;
  gap: 8px;
  margin-bottom: 9px;
}

.history-head h3 {
  margin: 0;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 1px;
  text-transform: uppercase;
  color: var(--muted);
}

.history-head wa-button {
  margin-left: auto;
}

.history-block {
  margin-bottom: 12px;
}

.history-block h2 {
  margin: 0 0 5px;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.9px;
  text-transform: uppercase;
  color: var(--muted-dim);
}

.history-note {
  margin: 5px 0 0;
  font-size: 11px;
  color: var(--muted-dim);
}

.timeline .ctx-none,
.snapshots .ctx-none {
  margin: 0;
}

.tl-strip {
  display: flex;
  gap: 2px;
  height: 14px;
  overflow: hidden;
}

.tl-bar {
  min-width: 3px;
}

.tl-bar--valid {
  background: var(--valid);
}

.tl-bar--warning {
  background: var(--warning);
}

.tl-bar--invalid {
  background: var(--invalid);
}

.tl-bar--parse {
  background: var(--muted-dim);
}

.snapshots {
  display: flex;
  flex-direction: column;
  gap: 3px;
}

.snapshot {
  display: flex;
  align-items: center;
  gap: 7px;
  padding: 5px 7px;
  border-left: 2px solid var(--hairline);
  background: var(--panel-2);
}

.snapshot-meta {
  display: flex;
  flex-direction: column;
  gap: 1px;
  min-width: 0;
}

.snapshot-name {
  font-size: 11px;
  color: var(--text);
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.snapshot-sub {
  font-size: 11px;
  color: var(--muted-dim);
}

.snapshot-actions {
  margin-left: auto;
  display: flex;
  gap: 3px;
  flex: 0 0 auto;
}

.history-actions {
  display: flex;
  flex-wrap: wrap;
  gap: 5px;
  padding-top: 9px;
  border-top: 1px solid var(--hairline);
}

/* =========================================================================
   File drop
   ========================================================================= */

.drop-overlay {
  position: absolute;
  inset: 6px;
  z-index: 25;
  display: grid;
  place-items: center;
  /* Must not swallow the drop event itself. */
  pointer-events: none;
  border: 2px dashed var(--accent);
  background: var(--accent-bg);
  color: var(--accent);
  font-size: 12px;
  font-weight: 600;
}

.drop-overlay[hidden] {
  display: none;
}

.drop-overlay p {
  margin: 0;
}

/* =========================================================================
   Export dialog (contents of a <wa-dialog>)
   ========================================================================= */

.dialog-body {
  padding: 12px;
  display: flex;
  flex-direction: column;
  gap: 10px;
}

.dialog-options {
  display: flex;
  flex-wrap: wrap;
  align-items: flex-start;
  gap: 6px 22px;
}

.latex-textarea {
  width: 100%;
  height: 200px;
  font-family: var(--font-mono);
  font-size: 12px;
  line-height: 1.5;
  background: var(--bg);
  color: var(--text);
  border: 1px solid var(--border);
  padding: 8px;
  resize: vertical;
}

.latex-textarea:focus {
  outline: 2px solid var(--accent);
  outline-offset: -2px;
}

.dialog-note {
  margin: 0;
  max-width: 68ch;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.5;
  color: var(--muted);
}

.dialog-actions {
  display: flex;
  align-items: center;
  justify-content: flex-end;
  gap: 6px;
}

/* --- Pack dialog: a folder's details as a pack ----------------------------- */

.pack-dialog {
  --width: min(760px, calc(100vw - 32px));
}

.pack-form {
  display: flex;
  flex-direction: column;
  gap: 22px;
}

.pack-fields {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
  gap: 12px 16px;
  margin: 0;
  padding: 0;
  border: 0;
  min-width: 0;
}

.pack-fields legend {
  grid-column: 1 / -1;
  margin: 0 0 10px;
  padding: 0;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
}

.pack-summary-field {
  grid-column: 1 / -1;
  display: flex;
  flex-direction: column;
  gap: 4px;
}

/* Matches the label <wa-input> draws for the fields beside it. */
.pack-label {
  font-size: var(--wa-form-control-label-font-size, 13px);
  font-weight: var(--wa-form-control-label-font-weight, 600);
  color: var(--wa-form-control-label-color, var(--text));
}

.pack-cell-label {
  font-size: 12px;
  color: var(--muted);
}

.pack-textarea,
.pack-input {
  width: 100%;
  min-width: 0;
  padding: 4px 8px;
  border: 1px solid var(--app-control-border);
  border-radius: var(--radius);
  background: var(--bg);
  color: var(--text);
  font: inherit;
  font-size: 13px;
}

.pack-textarea {
  font-family: var(--font-prose);
  line-height: 1.5;
  resize: vertical;
}

.pack-input {
  box-sizing: border-box;
  height: 28px;
}

.pack-textarea:focus,
.pack-input:focus {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -1px;
  border-color: transparent;
}

.pack-entries {
  grid-template-columns: minmax(0, 1fr);
  gap: 0;
}

.pack-empty {
  margin: 0;
  font-family: var(--font-prose);
  font-size: 13px;
  color: var(--muted);
}

/* One proof per row: its file, then the details it is listed under. */
.pack-entry {
  display: grid;
  grid-template-columns: 8em minmax(0, 1.4fr) minmax(0, 1fr) 6.5em;
  gap: 6px 10px;
  padding: 12px 0;
  border-top: 1px solid var(--hairline);
}

.pack-entry-file {
  grid-column: 1 / -1;
  margin: 0;
  font-size: 12px;
  font-weight: 600;
}

.pack-cell {
  display: flex;
  flex-direction: column;
  gap: 3px;
  min-width: 0;
}

.pack-cell--explain {
  grid-column: 1 / -1;
  display: none;
}

.pack-entry.is-trap .pack-cell--explain {
  display: flex;
}

.pack-dialog-actions {
  flex-wrap: wrap;
}

.pack-dialog::part(footer) {
  border-top: 1px solid var(--border);
}

.pack-status {
  flex: 1 1 100%;
  font-family: var(--font-prose);
  font-size: 13px;
  color: var(--muted);
}

.pack-status:empty {
  display: none;
}

.pack-status p,
.pack-problems {
  margin: 0;
}

.pack-problems {
  padding-left: 1.2em;
}

.pack-status[data-tone="invalid"] {
  color: var(--invalid);
}

.pack-status[data-tone="valid"] {
  color: var(--valid);
}

/* =========================================================================
   Panel arrangement
   ========================================================================= */

/* The grip is the drag handle: six dots, quiet until touched.  It is a real
   button rather than a decoration, so it is reachable by Tab and the arrow
   keys can be bound to it -- a drag is not the only way to move a panel. */
.pane-grip {
  flex: none;
  display: grid;
  place-items: center;
  width: 14px;
  height: 16px;
  padding: 0;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--muted-dim);
  font-size: 11px;
  cursor: grab;
}

.pane-grip:hover,
.pane-grip:focus-visible {
  color: var(--text);
  background: var(--panel-2);
}

.pane-grip:active {
  cursor: grabbing;
}

.layout-panel {
  display: block;
  width: 268px;
  max-width: calc(100vw - 28px);
  padding: 10px;
  background: var(--panel);
  border: 1px solid var(--border);
}

.layout-panel h2 {
  margin: 0 0 8px;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 1px;
  text-transform: uppercase;
  color: var(--muted);
}

.layout-options {
  display: flex;
  flex-direction: column;
  gap: 1px;
}

/* A menu row: the name and what it does on the left, a miniature of the
   result on the right. */
.layout-option {
  display: grid;
  grid-template-columns: minmax(0, 1fr) 34px;
  grid-template-rows: auto auto;
  align-items: center;
  gap: 0 10px;
  padding: 6px 7px;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--text);
  font-family: inherit;
  font-size: 11px;
  text-align: left;
  cursor: pointer;
}

.layout-option:hover,
.layout-option:focus-visible {
  background: var(--panel-2);
}

.layout-option[data-active="true"] {
  background: var(--accent-bg);
}

.layout-option-label {
  grid-column: 1;
  grid-row: 1;
  font-weight: 600;
}

.layout-option-hint {
  grid-column: 1;
  grid-row: 2;
  font-size: 11px;
  color: var(--muted);
}

.layout-preview {
  grid-column: 2;
  grid-row: 1 / span 2;
  width: 34px;
  height: 22px;
}

/* Hairline boxes; the slot the arrangement is *about* carries the accent, so
   four small pictures stay tellable apart at a glance. */
.layout-preview rect {
  fill: none;
  stroke: var(--border);
  stroke-width: 1.5;
}

.layout-preview rect[data-accent] {
  fill: var(--accent-bg);
  stroke: var(--accent);
}

/* =========================================================================
   The shell: rail, views, status bar
   ========================================================================= */

.skip-link {
  position: absolute;
  left: 52px;
  top: 6px;
  z-index: 40;
  padding: 4px 8px;
  background: var(--bg);
  color: var(--accent);
  border: 1px solid var(--accent);
  border-radius: var(--radius);
  font-size: 12px;
  transform: translateY(-200%);
}

.skip-link:focus {
  transform: none;
}

/* Elements given a display below would otherwise ignore [hidden]. */
[hidden] {
  display: none !important;
}

/* The rail: four views and two global controls.  A column of quiet glyphs;
   the current view's icon takes the accent on a lowered square (see below). */
.rail {
  grid-area: rail;
  display: flex;
  flex-direction: column;
  align-items: stretch;
  gap: 2px;
  padding: 8px 0;
  background: var(--panel);
  border-right: 1px solid var(--border);
  min-height: 0;
}

.rail-mark {
  display: grid;
  place-items: center;
  height: 28px;
  margin-bottom: 8px;
  font-size: 15px;
  font-weight: 700;
  color: var(--text);
  letter-spacing: -0.02em;
}

.rail-views,
.rail-end {
  display: flex;
  flex-direction: column;
  gap: 2px;
}

.rail-end {
  margin-top: auto;
}

.rail-button {
  position: relative;
  display: grid;
  place-items: center;
  height: 40px;
  margin: 0 4px;
  padding: 0;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--muted);
  font: inherit;
  cursor: pointer;
}

.rail-button .icon {
  width: 18px;
  height: 18px;
}

.rail-button:hover {
  color: var(--text);
  background: var(--panel-2);
}

.rail-button:focus-visible {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -2px;
}

.rail-button[aria-current="page"] {
  color: var(--accent);
}

/* The current view: the icon in the accent on a lowered square.  The left
   margin belongs to the failure rail, so nothing else draws a rule there. */
.rail-button[aria-current="page"]::before {
  content: "";
  position: absolute;
  left: 50%;
  top: 50%;
  width: 28px;
  height: 28px;
  transform: translate(-50%, -50%);
  border-radius: var(--radius);
  background: var(--panel-2);
}

.rail-button .icon {
  position: relative;
}

/* The labels are for the narrow layout, where the rail turns into a bar
   along the foot; beside the views the glyph and its aria-label suffice. */
.rail-label {
  display: none;
}

.rail-button--quiet {
  height: 32px;
}

.rail-button--quiet .icon {
  width: 16px;
  height: 16px;
}

.view {
  grid-area: view;
  min-width: 0;
  min-height: 0;
}

/* -------------------------------------------------------------------------
   Workspace: the desk (reading pane) beside the work
   ------------------------------------------------------------------------- */

.view--workspace {
  display: grid;
  grid-template-columns: 320px minmax(0, 1fr);
  transition: grid-template-columns 180ms ease;
}

html[data-desk="closed"] .view--workspace {
  grid-template-columns: 0 minmax(0, 1fr);
}

html[data-desk="closed"] .desk {
  visibility: hidden;
}

.desk {
  display: flex;
  flex-direction: column;
  min-width: 0;
  min-height: 0;
  overflow: hidden;
  background: var(--bg);
  border-right: 1px solid var(--border);
}

.desk-head {
  display: flex;
  align-items: stretch;
  gap: 4px;
  padding: 0 6px 0 4px;
  min-height: 34px;
  border-bottom: 1px solid var(--border);
  flex: none;
}

.desk-tabs {
  display: flex;
  align-items: stretch;
  gap: 2px;
  flex: 1 1 auto;
  min-width: 0;
}

/* Tabs are labels with a rule under the chosen one -- no boxes. */
.desk-tab {
  position: relative;
  padding: 0 9px;
  border: 0;
  background: none;
  color: var(--muted);
  font: inherit;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  cursor: pointer;
}

.desk-tab:hover {
  color: var(--text);
}

.desk-tab[aria-selected="true"] {
  color: var(--text);
}

.desk-tab[aria-selected="true"]::after {
  content: "";
  position: absolute;
  left: 9px;
  right: 9px;
  bottom: -1px;
  height: 2px;
  background: var(--accent);
}

.desk-tab:focus-visible {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -4px;
}

.desk-head > .icon-button-native {
  align-self: center;
}

.desk-panel {
  display: flex;
  flex-direction: column;
  flex: 1 1 auto;
  min-height: 0;
}

.desk-tools {
  display: flex;
  align-items: center;
  gap: 2px;
  padding: 5px 6px;
  border-bottom: 1px solid var(--hairline);
  flex: none;
}

.desk-tools-spacer,
.toolstrip-spacer,
.status-spacer {
  flex: 1 1 auto;
}

/* -------------------------------------------------------------------------
   Native buttons: one icon button, one text button, used everywhere a Web
   Awesome button would be heavier than the job.
   ------------------------------------------------------------------------- */

.icon-button-native {
  display: inline-grid;
  place-items: center;
  width: 24px;
  height: 24px;
  padding: 0;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--muted);
  cursor: pointer;
  flex: none;
}

.icon-button-native .icon {
  width: 14px;
  height: 14px;
}

.icon-button-native:hover {
  color: var(--text);
  background: var(--panel-2);
}

.icon-button-native:focus-visible,
.text-button:focus-visible,
.symbol:focus-visible,
.filter:focus-visible,
.pack-button:focus-visible,
.entry-head:focus-visible,
.status-button:focus-visible,
.toast-action:focus-visible {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -2px;
}

.text-button {
  display: inline-flex;
  align-items: center;
  gap: 5px;
  height: 24px;
  padding: 0 8px;
  border: 1px solid transparent;
  border-radius: var(--radius);
  background: none;
  color: var(--text);
  font: inherit;
  font-size: 12px;
  white-space: nowrap;
  cursor: pointer;
}

.text-button:hover {
  background: var(--panel-2);
}

.text-button--primary {
  color: var(--accent);
  border-color: color-mix(in oklab, var(--accent) 45%, transparent);
}

.text-button--primary:hover {
  background: var(--accent-bg);
}

.text-button:disabled {
  color: var(--muted-dim);
  border-color: transparent;
  background: none;
  cursor: default;
}

.text-button--danger {
  color: var(--danger-text);
}

.text-button--danger:hover {
  background: var(--invalid-bg);
}

/* The second click of a two-click confirmation. */
.text-button.is-armed {
  color: var(--wa-color-danger-on-loud, #fff);
  background: var(--wa-color-danger-fill-loud);
  border-color: var(--wa-color-danger-fill-loud);
}

.text-button--menu::after {
  content: "";
  width: 0;
  height: 0;
  margin-left: 2px;
  border: 3.5px solid transparent;
  border-top-color: currentColor;
  border-bottom-width: 0;
}

/* -------------------------------------------------------------------------
   Explorer
   ------------------------------------------------------------------------- */

.explorer {
  padding: 4px 0 12px;
}

.tree-row {
  display: flex;
  align-items: center;
  gap: 6px;
  height: 26px;
  padding: 0 6px 0 calc(10px + var(--depth, 0) * 14px);
  color: var(--text);
  font-size: 12px;
  cursor: pointer;
  user-select: none;
}

.tree-row .icon {
  width: 14px;
  height: 14px;
  flex: none;
  color: var(--muted-dim);
}

.tree-row--folder .tree-label {
  color: var(--muted);
}

/* A folder that is a pack says so, in words. */
.tree-tag {
  flex: none;
  font-size: 11px;
  color: var(--muted-dim);
}

.tree-label {
  flex: 1 1 auto;
  min-width: 0;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.tree-row:hover {
  background: var(--panel-2);
}

.tree-row.is-active {
  background: var(--accent-bg);
}

.tree-row.is-active .tree-label {
  color: var(--accent);
}

.tree-row:focus-visible {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -2px;
}

.tree-row[data-drop-target] {
  outline: 1px dashed var(--accent);
  outline-offset: -1px;
  background: var(--accent-bg);
}

/* The verdict of the file's last check.  Valid is unmarked, as everywhere. */
.tree-mark,
.tab-mark {
  width: 6px;
  height: 6px;
  border-radius: 50%;
  flex: none;
}

.tree-mark--warning,
.tab-mark--warning {
  background: var(--warning);
}

.tree-mark--invalid,
.tab-mark--invalid,
.tree-mark--parse,
.tab-mark--parse {
  background: var(--invalid);
}

.tree-actions {
  display: none;
  gap: 1px;
  flex: none;
}

.tree-row:hover .tree-actions,
.tree-row:focus-within .tree-actions,
.tree-row.is-active .tree-actions {
  display: flex;
}

.tree-action {
  display: grid;
  place-items: center;
  width: 20px;
  height: 20px;
  padding: 0;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--muted);
  cursor: pointer;
}

.tree-action .icon {
  width: 12px;
  height: 12px;
  color: inherit;
}

.tree-action:hover {
  color: var(--text);
  background: var(--panel-3);
}

.tree-rename {
  flex: 1 1 auto;
  min-width: 0;
  height: 20px;
  padding: 0 4px;
  border: 1px solid var(--accent);
  border-radius: var(--radius);
  background: var(--bg);
  color: var(--text);
  font: inherit;
  font-size: 12px;
  outline: none;
}

.tree-empty,
.notes-empty,
.library-empty {
  padding: 18px 14px;
  font-family: var(--font-prose);
  font-size: 13px;
  color: var(--text);
}

.tree-empty p,
.notes-empty p,
.library-empty p {
  margin: 0 0 6px;
}

.tree-empty-sub,
.notes-empty-sub,
.library-empty-sub {
  color: var(--muted);
  font-size: 12px;
  line-height: 1.5;
}

.notes-empty .text-button {
  margin-top: 6px;
  font-family: var(--font-mono);
}

/* -------------------------------------------------------------------------
   The work: tab strip, tool strip, the three panes
   ------------------------------------------------------------------------- */

.work {
  display: flex;
  flex-direction: column;
  min-width: 0;
  min-height: 0;
}

.work-head {
  display: flex;
  align-items: stretch;
  min-height: 34px;
  background: var(--panel);
  border-bottom: 1px solid var(--border);
  flex: none;
}

.work-head > .icon-button-native {
  align-self: center;
  margin: 0 2px 0 6px;
}

.tabs {
  display: flex;
  align-items: stretch;
  min-width: 0;
  overflow-x: auto;
  scrollbar-width: none;
}

.tab {
  position: relative;
  display: flex;
  align-items: center;
  gap: 7px;
  max-width: 220px;
  padding: 0 6px 0 12px;
  border-right: 1px solid var(--hairline);
  color: var(--muted);
  font-size: 12px;
  white-space: nowrap;
  cursor: pointer;
  user-select: none;
}

.tab:hover {
  color: var(--text);
}

/* The open proof's tab joins the page below it: same paper, no rule. */
.tab.is-active {
  color: var(--text);
  background: var(--bg);
  margin-bottom: -1px;
}

.tab.is-active::before {
  content: "";
  position: absolute;
  left: 0;
  right: 0;
  top: 0;
  height: 2px;
  background: var(--accent);
}

.tab:focus-visible {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -2px;
}

.tab-mark:not([class*="--"]) {
  display: none;
}

.tab-label {
  overflow: hidden;
  text-overflow: ellipsis;
}

.tab-close {
  display: grid;
  place-items: center;
  width: 18px;
  height: 18px;
  padding: 0;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--muted-dim);
  visibility: hidden;
  cursor: pointer;
}

.tab-close .icon {
  width: 11px;
  height: 11px;
}

.tab:hover .tab-close,
.tab.is-active .tab-close,
.tab:focus-within .tab-close {
  visibility: visible;
}

.tab-close:hover {
  color: var(--text);
  background: var(--panel-2);
}

.tabs-empty {
  align-self: center;
  padding: 0 12px;
  font-size: 12px;
  color: var(--muted-dim);
}

.toolstrip {
  display: flex;
  align-items: center;
  gap: 6px;
  min-height: 32px;
  padding: 3px 8px;
  border-bottom: 1px solid var(--border);
  flex: none;
  overflow-x: auto;
  scrollbar-width: none;
}

.toolstrip-rule {
  width: 1px;
  height: 16px;
  background: var(--border);
  flex: none;
}

.symbols {
  display: flex;
  align-items: center;
  gap: 1px;
  padding-left: 6px;
  margin-left: 2px;
  border-left: 1px solid var(--hairline);
}

/* Each symbol is set at the size it will appear in the proof. */
.symbol {
  display: grid;
  place-items: center;
  min-width: 22px;
  height: 22px;
  padding: 0 3px;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--text);
  font: inherit;
  font-size: 13px;
  cursor: pointer;
}

.symbol:hover {
  background: var(--panel-2);
  color: var(--accent);
}

.dropdown-detail {
  display: block;
  font-size: 11px;
  color: var(--muted);
}

.toolstrip-dropdown wa-dropdown-item {
  font-size: 12px;
}

.pane--editor {
  position: relative;
}

.exercise-banner {
  padding: 7px 12px;
  border-bottom: 1px solid var(--hairline);
  border-left: 2px solid var(--accent);
  background: var(--accent-bg);
  font-family: var(--font-prose);
  font-size: 12px;
  color: var(--text);
}

/* No proof open: the editor's place holds a short way in. */
.welcome {
  flex: 1 1 auto;
  display: grid;
  place-items: center;
  padding: 24px;
}

.welcome-box {
  max-width: 380px;
}

.welcome-box h2 {
  margin: 0 0 6px;
  font-size: 13px;
  font-weight: 700;
}

.welcome-box p {
  margin: 0 0 14px;
  font-family: var(--font-prose);
  font-size: 13px;
  color: var(--muted);
  line-height: 1.55;
}

.welcome-actions {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
}

/* -------------------------------------------------------------------------
   Notes (the desk's middle tab)
   ------------------------------------------------------------------------- */

.notes {
  padding: 0 0 16px;
}

.note-entry,
.note-pinned,
.welcome-card {
  padding: 14px 14px 16px;
  border-bottom: 1px solid var(--hairline);
}

/* Where an entry comes from: a quiet line after its title, never a label
   above it. */
.note-source {
  margin: -4px 0 12px;
  font-size: 11px;
  color: var(--muted);
}

/* "Example 2.18": the notes' own numbering is the heading. */
.note-ref {
  margin: 0;
  font-size: 13px;
  font-weight: 700;
  color: var(--text);
}

.note-title {
  margin: 2px 0 10px;
  font-family: var(--font-mono);
  font-size: 14px;
  font-weight: 600;
  line-height: 1.35;
  color: var(--text);
}

.note-text {
  margin: 0 0 10px;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.6;
  color: var(--text);
}

.note-subhead {
  margin: 14px 0 6px;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
}

.note-pick {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 6px;
  margin: 4px 0 6px;
  padding: 8px 0 0;
  border-top: 1px solid var(--hairline);
}

.note-pick-label {
  flex: 1 0 100%;
  font-size: 12px;
  color: var(--muted);
  font-variant-numeric: tabular-nums;
}

/* The answer, in the auditor's language: a rail and a sentence. */
.note-verdict {
  margin: 0 0 10px;
  padding: 2px 0 2px 10px;
  border-left: 2px solid;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.5;
}

.note-verdict.is-right {
  color: var(--valid);
  border-left-color: var(--valid);
}

.note-verdict.is-wrong {
  color: var(--invalid);
  border-left-color: var(--invalid);
}

.note-tools {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
  margin-top: 12px;
  margin-left: -8px;
}

.note-pinned-head {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 8px;
  margin-bottom: 6px;
}

.note-pinned-head .note-ref {
  margin: 0;
}

.welcome-card h2 {
  margin: 0 0 6px;
  font-size: 13px;
  font-weight: 700;
}

.welcome-card > p {
  margin: 0 0 10px;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.55;
  color: var(--muted);
}

.welcome-steps {
  margin: 0 0 12px;
  padding: 0 0 0 22px;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.5;
}

.welcome-steps li {
  padding: 3px 4px;
  border-radius: var(--radius);
  cursor: default;
}

.welcome-steps li::marker {
  font-family: var(--font-mono);
  font-size: 11px;
  color: var(--muted);
}

.welcome-steps li:hover,
.welcome-steps li:focus-visible {
  background: var(--accent-bg);
  outline: none;
}

/* While a tour step is hovered, the region it names is outlined. */
[data-tour="on"] {
  outline: 2px solid var(--accent) !important;
  outline-offset: -2px;
}

/* An exercise hides the answer: the auditor's verdicts, messages and rails,
   and the counterexamples.  The statements stay, so the student can read the
   proof in the auditor's normalised form. */
body[data-exercise="hidden"] .step-meta,
body[data-exercise="hidden"] .step-message,
body[data-exercise="hidden"] .note,
body[data-exercise="hidden"] .report-verdict {
  display: none;
}

body[data-exercise="hidden"] .step::before {
  background: transparent;
}

.verdict--exercise {
  color: var(--accent);
  border-left-color: var(--accent);
}

/* -------------------------------------------------------------------------
   Full views: Library, Guide, Settings
   ------------------------------------------------------------------------- */

.view--page {
  overflow: auto;
  background: var(--bg);
}

.page {
  max-width: 1080px;
  margin: 0 auto;
  padding: 28px 32px 56px;
}

.page--narrow {
  max-width: 720px;
}

.page-head {
  margin-bottom: 20px;
}

/* A page title, not a label: it has to outrank the uppercase section labels
   beneath it. */
.page-head h1 {
  margin: 0 0 8px;
  font-family: var(--font-mono);
  font-size: 20px;
  font-weight: 600;
  line-height: 1.25;
  color: var(--text);
}

.page-lede {
  margin: 0;
  max-width: 62ch;
  font-family: var(--font-prose);
  font-size: 14px;
  line-height: 1.55;
  color: var(--muted);
}

/* Segmented control: Library filters and every choice in Settings. */
.filters {
  display: inline-flex;
  flex: none;
  border: 1px solid var(--border);
  border-radius: var(--radius);
}

.filter {
  height: 24px;
  padding: 0 10px;
  border: 0;
  border-right: 1px solid var(--border);
  background: none;
  color: var(--muted);
  font: inherit;
  font-size: 12px;
  cursor: pointer;
  font-variant-numeric: tabular-nums;
}

.filter:last-child {
  border-right: 0;
}

.filter:hover {
  color: var(--text);
}

.filter[aria-checked="true"] {
  color: var(--accent);
  background: var(--accent-bg);
}

/* --- Library -------------------------------------------------------------- */

.library-controls {
  display: flex;
  align-items: center;
  gap: 12px;
  margin-bottom: 18px;
}

.library-search {
  flex: 1 1 auto;
  max-width: 520px;
}

/* Labelled for assistive technology; the placeholder and the page heading
   already say what the field is for on screen. */
.library-search::part(form-control-label) {
  position: absolute;
  width: 1px;
  height: 1px;
  overflow: hidden;
  clip: rect(0, 0, 0, 0);
  white-space: nowrap;
}

.library-body {
  display: grid;
  grid-template-columns: 220px minmax(0, 1fr);
  gap: 28px;
  align-items: start;
}

.library-packs {
  position: sticky;
  top: 0;
  display: flex;
  flex-direction: column;
  gap: 1px;
}

.pack-button {
  position: relative;
  display: grid;
  grid-template-columns: minmax(0, 1fr) auto;
  gap: 0 8px;
  padding: 7px 10px;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--text);
  font: inherit;
  text-align: left;
  cursor: pointer;
}

.pack-button:hover {
  background: var(--panel-2);
}

.pack-button[aria-current="true"] {
  background: var(--panel-2);
}

.pack-code {
  font-size: 12px;
  font-weight: 700;
}

.pack-button[aria-current="true"] .pack-code {
  color: var(--accent);
}

.pack-title {
  grid-column: 1;
  font-family: var(--font-prose);
  font-size: 12px;
  color: var(--muted);
}

.pack-count {
  grid-column: 2;
  grid-row: 1 / span 2;
  align-self: center;
  font-size: 11px;
  color: var(--muted-dim);
  font-variant-numeric: tabular-nums;
}

/* "update": a word under the count, not a badge. */
.pack-flag {
  grid-column: 1 / -1;
  font-size: 11px;
  color: var(--accent);
}

.packs-actions {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
  margin: 0 0 14px;
}

/* Rail groups read like the chapter labels: small, set apart by space. */
.packs-group-head {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 8px;
}

.packs-group {
  margin: 14px 10px 6px;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
}

.packs-group-head .packs-group {
  margin-top: 0;
}

.packs-group-head .text-button {
  margin-bottom: 6px;
}

.library-list:focus {
  outline: none;
}

.pack + .pack {
  margin-top: 32px;
}

.pack-head h2 {
  margin: 0 0 4px;
  font-size: 14px;
  font-weight: 600;
  line-height: 1.35;
}

.pack-meta {
  margin: 0 0 8px;
  font-size: 12px;
  color: var(--muted);
  font-variant-numeric: tabular-nums;
}

.pack-actions {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
  /* The first button's word, not its padding, lines up with the title. */
  margin: -6px 0 18px -8px;
}

.pack-check {
  margin: -8px 0 18px;
  font-family: var(--font-prose);
  font-size: 13px;
  color: var(--muted);
}

.pack-check.is-invalid {
  color: var(--invalid);
}

.pack-note {
  margin: 0 0 16px;
  max-width: 68ch;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.55;
  color: var(--muted);
}

.chapter + .chapter {
  margin-top: 20px;
}

.chapter-title {
  margin: 0;
  padding: 0 0 6px;
  border-bottom: 1px solid var(--border);
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
  white-space: pre;
}

.entry {
  border-bottom: 1px solid var(--hairline);
}

.entry-head {
  display: grid;
  grid-template-columns: 9.5em minmax(0, 1fr) auto;
  align-items: baseline;
  gap: 12px;
  width: 100%;
  padding: 8px 6px;
  border: 0;
  background: none;
  color: var(--text);
  font: inherit;
  text-align: left;
  cursor: pointer;
}

.entry-head:hover {
  background: var(--panel);
}

.entry.is-open .entry-head {
  background: var(--panel);
}

/* A long reference ("Remark, Basic Properties 3") wraps in its column
   rather than running into the title. */
.entry-ref {
  font-size: 12px;
  font-weight: 600;
  color: var(--muted);
  font-variant-numeric: tabular-nums;
  overflow-wrap: anywhere;
}

.entry-title {
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.4;
}

.entry-tags {
  display: flex;
  gap: 6px;
}

.entry-tag {
  font-size: 11px;
  color: var(--muted);
  white-space: nowrap;
}

/* A trap is a kind of entry, like a theorem; red is kept for a copy that
   actually fails. */
.entry-tag--trap {
  color: var(--muted);
}

.entry-tag + .entry-tag::before {
  content: "·";
  margin-right: 6px;
  color: var(--muted-dim);
}

.entry-tag--copy.is-valid {
  color: var(--valid);
}

.entry-tag--copy.is-warning {
  color: var(--warning);
}

.entry-tag--copy.is-invalid,
.entry-tag--copy.is-parse {
  color: var(--invalid);
}

/* "Check all entries": quiet when an entry still gives its recorded verdict,
   red when it no longer does. */
.entry-tag--check.is-same {
  color: var(--muted-dim);
}

.entry-tag--check.is-invalid {
  color: var(--invalid);
}

.entry-blurb--quiet {
  color: var(--muted);
}

.entry-body {
  padding: 4px 6px 14px calc(9.5em + 18px);
  background: var(--panel);
}

.entry-blurb {
  margin: 0 0 10px;
  max-width: 68ch;
  font-family: var(--font-prose);
  font-size: 13px;
  line-height: 1.55;
  color: var(--text);
}

.entry-source {
  margin: 0 0 12px;
  padding: 10px 12px;
  max-height: 280px;
  overflow: auto;
  background: var(--bg);
  border: 1px solid var(--hairline);
  border-radius: var(--radius);
  font-family: var(--font-mono);
  font-size: 12px;
  line-height: 1.55;
  color: var(--text);
}

.entry-actions {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
}

/* --- Guide ---------------------------------------------------------------- */

.page--guide {
  display: grid;
  grid-template-columns: 200px minmax(0, 1fr);
  gap: 40px;
  align-items: start;
}

.guide-toc {
  position: sticky;
  top: 28px;
}

.guide-toc-head {
  margin: 0 0 8px;
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
}

.guide-toc-list {
  margin: 0;
  padding: 0;
  list-style: none;
}

.guide-toc-link {
  position: relative;
  display: block;
  padding: 4px 10px;
  border-radius: var(--radius);
  color: var(--muted);
  font-size: 12px;
  text-decoration: none;
}

.guide-toc-link:hover {
  color: var(--text);
  background: var(--panel-2);
}

.guide-toc-link[aria-current="page"] {
  color: var(--text);
  font-weight: 700;
}

.guide-toc-link:focus-visible {
  outline: 2px solid var(--wa-color-focus);
  outline-offset: -2px;
}

.guide-article {
  min-width: 0;
  max-width: 72ch;
}

.guide-tools {
  display: flex;
  justify-content: flex-end;
  margin-bottom: -22px;
}

/* The handbook reads as prose; code and the formal layer stay in mono. */
.guide-body {
  font-family: var(--font-prose);
  font-size: 14px;
  line-height: 1.65;
  color: var(--text);
}

.guide-body h1 {
  margin: 0 0 12px;
  font-family: var(--font-mono);
  font-size: 20px;
  font-weight: 600;
  line-height: 1.25;
}

.guide-body h2 {
  margin: 32px 0 8px;
  font-family: var(--font-mono);
  font-size: 13px;
  font-weight: 700;
}

.guide-body h3 {
  margin: 22px 0 6px;
  font-family: var(--font-mono);
  font-size: 12px;
  font-weight: 700;
  color: var(--muted);
}

.guide-body p,
.guide-body ul,
.guide-body ol {
  margin: 0 0 12px;
}

.guide-body ul,
.guide-body ol {
  padding-left: 22px;
}

.guide-body li + li {
  margin-top: 3px;
}

.guide-body .lede {
  font-size: 15px;
  line-height: 1.6;
  color: var(--muted);
}

.guide-body code,
.guide-body kbd {
  font-family: var(--font-mono);
  font-size: 0.86em;
}

.guide-body code {
  padding: 0 3px;
  background: var(--panel-2);
  border-radius: var(--radius);
}

.guide-body pre {
  margin: 0;
  padding: 10px 12px;
  overflow-x: auto;
  font-family: var(--font-mono);
  font-size: 12px;
  line-height: 1.55;
}

.guide-body a {
  color: var(--accent);
}

.guide-body--pinned {
  font-size: 13px;
}

.guide-body--pinned h1 {
  display: none;
}

.guide-body--pinned .try-bar {
  display: none;
}

.try-block {
  margin: 0 0 16px;
  border: 1px solid var(--hairline);
  border-radius: var(--radius);
  background: var(--panel);
}

.try-bar {
  display: flex;
  align-items: center;
  gap: 8px;
  padding: 3px 4px 3px 12px;
  border-top: 1px solid var(--hairline);
}

.try-expect {
  font-family: var(--font-mono);
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  padding-left: 7px;
  border-left: 2px solid var(--muted-dim);
  color: var(--muted);
}

.try-expect--valid {
  color: var(--valid);
  border-left-color: var(--valid);
}

.try-expect--warn {
  color: var(--warning);
  border-left-color: var(--warning);
}

.try-expect--invalid,
.try-expect--parse-error {
  color: var(--invalid);
  border-left-color: var(--invalid);
}

.try-bar .text-button {
  margin-left: auto;
  font-family: var(--font-mono);
}

.guide-table {
  width: 100%;
  margin: 0 0 16px;
  border-collapse: collapse;
  font-size: 13px;
}

.guide-table th,
.guide-table td {
  padding: 6px 10px 6px 0;
  border-bottom: 1px solid var(--hairline);
  text-align: left;
  vertical-align: top;
}

.guide-table th {
  font-family: var(--font-mono);
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
  border-bottom-color: var(--border);
}

.capability-area td {
  padding-top: 16px;
  font-family: var(--font-mono);
  font-size: 12px;
  font-weight: 700;
  color: var(--text);
}

.capability-name {
  display: block;
}

.capability-source {
  display: block;
  margin-top: 2px;
  padding: 0 !important;
  background: none !important;
  color: var(--muted);
  font-size: 11px !important;
  white-space: pre;
  overflow: hidden;
  text-overflow: ellipsis;
  max-width: 34ch;
}

.capability-verdict {
  font-family: var(--font-mono);
  font-size: 11px;
  font-weight: 700;
  white-space: nowrap;
}

.capability-verdict.is-valid {
  color: var(--valid);
}

.capability-verdict.is-warn,
.capability-verdict.is-warning {
  color: var(--warning);
}

.capability-verdict.is-invalid,
.capability-verdict.is-parse-error,
.capability-verdict.is-gap {
  color: var(--invalid);
}

.capability-note {
  color: var(--muted);
  font-size: 12px;
}

.guide-loading,
.guide-error {
  font-family: var(--font-prose);
  color: var(--muted);
}

.guide-error {
  color: var(--danger-text);
}

/* --- Settings ------------------------------------------------------------- */

.settings-group {
  margin-bottom: 28px;
}

.settings-group h2 {
  margin: 0;
  padding-bottom: 6px;
  border-bottom: 1px solid var(--border);
  font-size: 11px;
  font-weight: 700;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  color: var(--muted);
}

.setting {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 24px;
  padding: 12px 0;
  border-bottom: 1px solid var(--hairline);
}

.setting-text {
  display: flex;
  flex-direction: column;
  gap: 2px;
  min-width: 0;
}

.setting-label {
  font-size: 13px;
  color: var(--text);
}

.setting-hint {
  max-width: 52ch;
  font-family: var(--font-prose);
  font-size: 12px;
  line-height: 1.5;
  color: var(--muted);
}

/* -------------------------------------------------------------------------
   Command palette
   ------------------------------------------------------------------------- */

.palette {
  width: min(600px, calc(100vw - 32px));
  max-height: min(460px, calc(100vh - 120px));
  margin: 12vh auto auto;
  padding: 0;
  border: 1px solid var(--border);
  border-radius: var(--radius);
  background: var(--bg);
  color: var(--text);
  overflow: hidden;
}

.palette::backdrop {
  background: var(--wa-color-overlay-modal);
}

.palette[open] {
  display: flex;
}

.palette-box {
  display: flex;
  flex-direction: column;
  width: 100%;
  min-height: 0;
}

.palette-input {
  flex: none;
  width: 100%;
  height: 42px;
  padding: 0 14px;
  border: 0;
  border-bottom: 1px solid var(--border);
  background: none;
  color: var(--text);
  font: inherit;
  font-size: 13px;
  outline: none;
}

.palette-input::placeholder {
  color: var(--cm-placeholder);
}

.palette-list {
  flex: 1 1 auto;
  min-height: 0;
  margin: 0;
  padding: 4px;
  overflow: auto;
  list-style: none;
}

.palette-row {
  display: flex;
  align-items: baseline;
  gap: 10px;
  padding: 6px 10px;
  border-radius: var(--radius);
  font-size: 12px;
  cursor: pointer;
}

.palette-row.is-selected {
  background: var(--accent-bg);
}

.palette-kind {
  flex: none;
  width: 6.5em;
  font-size: 11px;
  color: var(--muted-dim);
}

.palette-row.is-selected .palette-kind {
  color: var(--accent);
}

.palette-label {
  flex: 0 1 auto;
  min-width: 0;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.palette-detail {
  flex: 1 1 auto;
  min-width: 0;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
  font-family: var(--font-prose);
  color: var(--muted);
}

.palette-shortcut {
  margin-left: auto;
  flex: none;
}

.palette-empty {
  padding: 14px 10px;
  font-family: var(--font-prose);
  font-size: 13px;
  color: var(--muted);
}

.palette-hint {
  flex: none;
  margin: 0;
  padding: 6px 12px;
  border-top: 1px solid var(--hairline);
  font-size: 11px;
  color: var(--muted-dim);
}

/* -------------------------------------------------------------------------
   Status bar
   ------------------------------------------------------------------------- */

.statusbar {
  grid-area: status;
  display: flex;
  align-items: center;
  gap: 14px;
  padding: 0 10px 0 12px;
  background: var(--panel);
  border-top: 1px solid var(--border);
  font-size: 11px;
  color: var(--muted);
  white-space: nowrap;
  min-width: 0;
  overflow: hidden;
}

.statusbar .verdict {
  padding-top: 0;
  padding-bottom: 0;
  line-height: 16px;
}

.status-item {
  font-variant-numeric: tabular-nums;
  overflow: hidden;
  text-overflow: ellipsis;
}

.status-item:empty {
  display: none;
}

#status-storage[data-ok="false"] {
  color: var(--warning);
}

.status-button {
  height: 18px;
  padding: 0 6px;
  border: 0;
  border-radius: var(--radius);
  background: none;
  color: var(--invalid);
  font: inherit;
  cursor: pointer;
}

.status-button:hover {
  background: var(--invalid-bg);
}

.toast-action {
  margin-left: 12px;
  padding: 0;
  border: 0;
  background: none;
  color: var(--accent);
  font: inherit;
  font-weight: 700;
  cursor: pointer;
}

.toast-action:hover {
  text-decoration: underline;
}

/* Toasts rise from just above the status bar, never over it.  Flat, on a
   hairline, with a plain close: the countdown ring is decoration here. */
#toast {
  bottom: 26px;
}

wa-toast-item::part(toast-item) {
  border-radius: var(--radius);
  font-size: 12px;
}

/* The margin belongs to failure: only caveat and failure toasts keep a rule,
   at the world's 2px. */
wa-toast-item {
  --accent-width: 0;
}

wa-toast-item[variant="warning"],
wa-toast-item[variant="danger"] {
  --accent-width: 2px;
}

wa-toast-item::part(progress-ring) {
  display: none;
}

wa-toast-item::part(close-button) {
  font-size: 11px;
}

/* --- Browser surfaces: the parts the page did not draw ------------------- */

::selection {
  background: var(--cm-selection-focused);
}

:root {
  accent-color: var(--accent);
  caret-color: var(--accent);
  scrollbar-color: color-mix(in oklab, var(--wa-color-text-normal) 22%, transparent) transparent;
}

a {
  text-underline-offset: 0.18em;
  text-decoration-thickness: 1px;
}

/* -------------------------------------------------------------------------
   Diagnostics in the editor: the auditor's rail, carried into the gutter
   ------------------------------------------------------------------------- */

.editor .cm-editor .cm-gutter-lint {
  width: 8px;
}

.editor .cm-editor .cm-gutter-lint .cm-gutterElement {
  padding: 0;
}

.editor .cm-editor .cm-lint-marker {
  width: 2px;
  height: 100%;
  min-height: 1.2em;
  margin-left: 3px;
  background-image: none;
  content: none;
}

.editor .cm-editor .cm-lint-marker-error {
  background: var(--invalid);
}

.editor .cm-editor .cm-lint-marker-warning {
  background: var(--warning);
}

.editor .cm-editor .cm-lint-marker-info {
  background: var(--accent);
}

/* The tooltip on a marked range: the auditor's message, in its voice. */
.cm-editor .cm-tooltip-lint {
  max-width: 460px;
}

.cm-editor .cm-diagnostic {
  padding: 6px 10px 6px 10px;
  font-family: var(--font-prose);
  font-size: 12px;
  line-height: 1.5;
}

.cm-editor .cm-diagnostic-error {
  border-left: 2px solid var(--invalid);
}

.cm-editor .cm-diagnostic-warning {
  border-left: 2px solid var(--warning);
}

/* An exercise hides the open file's verdict mark too. */
body[data-exercise="hidden"] .tab.is-active .tab-mark,
body[data-exercise="hidden"] .tree-row.is-active .tree-mark {
  visibility: hidden;
}

@media (prefers-reduced-motion: reduce) {
  .view--workspace,
  .step {
    transition: none;
  }
}

/* =========================================================================
   Responsive
   ========================================================================= */

/* Below 1100px the reading pane overlays the work instead of squeezing it. */
@media (max-width: 1100px) {
  .view--workspace,
  html[data-desk="closed"] .view--workspace {
    position: relative;
    grid-template-columns: minmax(0, 1fr);
  }

  .desk {
    position: absolute;
    inset: 0 auto 0 0;
    z-index: 20;
    width: min(320px, 86vw);
    border-right: 1px solid var(--border);
  }

  .work {
    grid-column: 1;
  }

  .library-body,
  .page--guide {
    grid-template-columns: minmax(0, 1fr);
    gap: 16px;
  }

  /* The packs fall into even columns; actions and group labels span them. */
  .library-packs {
    position: static;
    display: grid;
    grid-template-columns: repeat(auto-fill, minmax(200px, 1fr));
    gap: 1px 8px;
  }

  .packs-actions,
  .packs-group,
  .packs-group-head {
    grid-column: 1 / -1;
  }

  .guide-toc {
    position: static;
  }

  .guide-toc-list {
    display: flex;
    flex-wrap: wrap;
    gap: 2px;
  }
}

/* Narrow: the panes stack and scroll as one page; the rail becomes a bar. */
@media (max-width: 760px) {
  .pack-dialog-actions wa-button {
    flex: 1 1 0;
  }

  .pack-fields {
    grid-template-columns: minmax(0, 1fr);
  }

  .pack-entry {
    grid-template-columns: repeat(2, minmax(0, 1fr));
  }

  body {
    grid-template-columns: minmax(0, 1fr);
    grid-template-rows: minmax(0, 1fr) 44px 24px;
    grid-template-areas: "view" "rail" "status";
  }

  .rail {
    flex-direction: row;
    padding: 0 4px;
    border-right: 0;
    border-top: 1px solid var(--border);
  }

  .rail-mark {
    display: none;
  }

  .rail-views {
    flex-direction: row;
    flex: 1 1 auto;
  }

  .rail-views .rail-button {
    flex: 1 1 0;
    display: flex;
    flex-direction: column;
    gap: 1px;
    height: 42px;
    margin: 0;
  }

  .rail-label {
    display: block;
    font-size: 11px;
  }

  .rail-button[aria-current="page"]::before {
    display: none;
  }

  .rail-button[aria-current="page"] .rail-label {
    font-weight: 700;
  }

  .rail-end {
    flex-direction: row;
    margin: 0;
    align-items: center;
  }

  .rail-button--quiet {
    width: 36px;
    margin: 0;
  }

  .work {
    overflow: auto;
  }

  .layout[data-layout] {
    grid-template-columns: minmax(0, 1fr);
    grid-template-rows: none;
    grid-template-areas: none;
    flex: 0 0 auto;
  }

  .pane[data-slot] {
    grid-area: auto;
  }

  .pane-grip {
    cursor: pointer;
  }

  .pane--editor {
    height: 55vh;
  }

  .pane--audit,
  .pane--context {
    height: auto;
  }

  .pane--audit .scroll,
  .pane--context .scroll {
    flex: 0 0 auto;
    overflow: visible;
  }

  .pane-head .pane-note {
    display: none;
  }

  .symbols {
    display: none;
  }

  .page {
    padding: 20px 16px 40px;
  }

  .library-controls {
    flex-direction: column;
    align-items: stretch;
  }

  .library-search {
    max-width: none;
  }

  .entry-head {
    grid-template-columns: minmax(0, 1fr) auto;
    gap: 2px 10px;
  }

  .entry-ref {
    grid-column: 1;
  }

  .entry-title {
    grid-column: 1;
  }

  .entry-tags {
    grid-column: 2;
    grid-row: 1 / span 2;
  }

  .entry-body {
    padding-left: 6px;
  }

  .setting {
    flex-direction: column;
    align-items: flex-start;
    gap: 8px;
  }

  /* A phone has room for the verdict and the way to the problem; the counts,
     the caret position and the path wait for a wider screen. */
  #status-file,
  #status-storage,
  #status-pos,
  .statusbar .verdict-meta {
    display: none;
  }

  #toast {
    bottom: 70px;
  }
}