/* ===========================================================================
   Referee theme

   Loaded after Verso's `book.css` and `verso-vars.css`, so it can both redefine
   Verso's own custom properties and override the handful of places where its
   stylesheet hardcodes a colour.

   Everything visual derives from the token block below, which exists in a light
   and a dark variant. Verso ships no dark mode of its own, so the dark variant
   also has to reach into Verso's chrome (header, table of contents, code).
   =========================================================================== */

/* --------------------------------------------------------------- tokens --- */

:root {
  color-scheme: light;
  --site-dark: 0;

  --site-bg: #fcfcfd;
  --site-surface: #ffffff;
  --site-surface-2: #f5f6f8;
  --site-surface-3: #eceef2;
  --site-border: #e3e5ea;
  --site-border-strong: #ccd0d8;

  --site-ink: #14161a;
  --site-ink-2: #4b5159;
  --site-ink-3: #7c838e;

  --site-accent: #2f5d8c;
  --site-accent-hover: #1f4368;
  --site-accent-soft: #eaf1f8;

  --site-ok: #2c7a51;
  --site-ok-soft: #e9f4ee;
  --site-warn: #8a5a10;
  --site-warn-soft: #fbf1de;
  --site-warn-border: #e4c68a;

  /* Statement diffs. Not red/green: the two sides of a changed statement are the previous and the
     current wording, neither of which is an error, and a red statement reads as a broken one.
     Colour carries the distinction, and the strike-through carries it again for anyone who cannot
     use the colour. */
  --site-del: #8c3f52;
  --site-del-soft: #fbecef;
  --site-ins: #2f6b4f;
  --site-ins-soft: #e8f4ed;

  /* Declaration kinds. Muted enough to sit under text without shouting. */
  --site-kind-theorem: #3f6fa8;
  --site-kind-definition: #4a7c6f;
  --site-kind-structure: #7a6096;
  --site-kind-instance: #8a6b3d;

  --site-shadow: 0 1px 2px rgba(16, 20, 28, .04), 0 8px 24px -12px rgba(16, 20, 28, .10);
  --site-shadow-lift: 0 2px 4px rgba(16, 20, 28, .06), 0 14px 32px -14px rgba(16, 20, 28, .18);

  --site-radius: 10px;
  --site-radius-sm: 6px;
  --site-measure: 78rem;

  /* ---- Verso's own variables, restated ---- */
  --verso-text-font-family: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, sans-serif;
  --verso-structure-font-family: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, sans-serif;
  --verso-code-font-family: ui-monospace, SFMono-Regular, "SF Mono", "JetBrains Mono", "Iosevka Term", Menlo, Consolas, monospace;

  --verso-text-color: var(--site-ink);
  --verso-code-color: var(--site-ink);
  --verso-structure-color: var(--site-ink);
  --verso-selected-color: var(--site-accent-soft);
  --verso-toc-background-color: var(--site-surface-2);
  /* Verso's search stylesheet reads this but never defines it, so it falls back to white and the
     search box stays light in dark mode. Defining it here is enough to theme the whole combobox. */
  --verso-background-color: var(--site-surface);

  --verso-code-const-color: #2b5f7d;
  --verso-code-const-weight: 500;
  --verso-code-keyword-color: #8a4a86;
  --verso-code-keyword-weight: 600;
  --verso-code-var-color: #7a5a2e;
  --verso-code-var-style: normal;

  --verso-error-color: #b3261e;
  --verso-warning-color: var(--site-warn);
  --verso-info-color: var(--site-ink-2);
}

@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    color-scheme: dark;
    --site-dark: 1;

    --site-bg: #0e1013;
    --site-surface: #15181d;
    --site-surface-2: #1a1e24;
    --site-surface-3: #222731;
    --site-border: #272c34;
    --site-border-strong: #3a414c;

    --site-ink: #e7eaee;
    --site-ink-2: #aab2bd;
    --site-ink-3: #79818d;

    --site-accent: #82b1e0;
    --site-accent-hover: #a8caee;
    --site-accent-soft: #16222e;

    --site-ok: #6cc08b;
    --site-ok-soft: #14231b;
    --site-warn: #e0b25e;
    --site-warn-soft: #241d10;
    --site-warn-border: #5a4620;

    --site-del: #e08a9c;
    --site-del-soft: #2a151a;
    --site-ins: #7fc3a1;
    --site-ins-soft: #142219;

    --site-kind-theorem: #7fa9d8;
    --site-kind-definition: #74b3a2;
    --site-kind-structure: #ab93c6;
    --site-kind-instance: #c2a06a;

    --site-shadow: 0 1px 2px rgba(0, 0, 0, .4), 0 10px 28px -14px rgba(0, 0, 0, .7);
    --site-shadow-lift: 0 2px 6px rgba(0, 0, 0, .5), 0 18px 40px -16px rgba(0, 0, 0, .8);

    --verso-code-const-color: #8fc3dd;
    --verso-code-keyword-color: #cf9fcb;
    --verso-code-var-color: #d7b98a;
    --verso-error-color: #f2857c;
  }
}

/* The toggle wins over the media query in both directions. */
:root[data-theme="dark"] {
  color-scheme: dark;
  --site-dark: 1;

  --site-bg: #0e1013;
  --site-surface: #15181d;
  --site-surface-2: #1a1e24;
  --site-surface-3: #222731;
  --site-border: #272c34;
  --site-border-strong: #3a414c;

  --site-ink: #e7eaee;
  --site-ink-2: #aab2bd;
  --site-ink-3: #79818d;

  --site-accent: #82b1e0;
  --site-accent-hover: #a8caee;
  --site-accent-soft: #16222e;

  --site-ok: #6cc08b;
  --site-ok-soft: #14231b;
  --site-warn: #e0b25e;
  --site-warn-soft: #241d10;
  --site-warn-border: #5a4620;

  --site-del: #e08a9c;
  --site-del-soft: #2a151a;
  --site-ins: #7fc3a1;
  --site-ins-soft: #142219;

  --site-kind-theorem: #7fa9d8;
  --site-kind-definition: #74b3a2;
  --site-kind-structure: #ab93c6;
  --site-kind-instance: #c2a06a;

  --site-shadow: 0 1px 2px rgba(0, 0, 0, .4), 0 10px 28px -14px rgba(0, 0, 0, .7);
  --site-shadow-lift: 0 2px 6px rgba(0, 0, 0, .5), 0 18px 40px -16px rgba(0, 0, 0, .8);

  --verso-code-const-color: #8fc3dd;
  --verso-code-keyword-color: #cf9fcb;
  --verso-code-var-color: #d7b98a;
  --verso-error-color: #f2857c;
}

/* ----------------------------------------------------------- base/layout --- */

html {
  background: var(--site-bg);
}

body {
  background: var(--site-bg);
  color: var(--site-ink);
  font-feature-settings: "kern" 1, "liga" 1;
  -webkit-font-smoothing: antialiased;
}

/* Verso hardcodes a white header with a grey shadow. */
header {
  background: color-mix(in srgb, var(--site-bg) 82%, transparent);
  backdrop-filter: saturate(1.6) blur(10px);
  border-bottom: 1px solid var(--site-border);
  box-shadow: none;
}

.header-title h1 {
  font-size: 1rem;
  font-weight: 600;
  letter-spacing: -0.01em;
}

.header-title,
.header-title:hover {
  color: var(--site-ink);
  text-decoration: none;
}

#toc {
  background: var(--site-surface-2);
  border-right: 1px solid var(--site-border);
}

#toc a {
  color: var(--site-ink-2);
  text-decoration: none;
}

#toc a:hover {
  color: var(--site-accent);
}

.toc-title h1 {
  font-size: .95rem;
  letter-spacing: -0.01em;
}

#meta-links a {
  color: var(--site-ink-3);
  font-size: .85rem;
}

.toc-resize-handle::after {
  background: var(--site-border);
}

/* Content is given room — declaration signatures are wide — but not unbounded. */
@media screen and (min-width: 900px) {
  .content-wrapper {
    box-sizing: border-box;
    margin: 0;
    max-width: none;
    width: 100%;
  }

  .content-wrapper > section,
  main section {
    box-sizing: border-box;
    max-width: var(--site-measure);
    min-width: 0;
    width: 100%;
  }
}

/* --------------------------------------------------------------- typography */

h1, h2, h3, h4 {
  letter-spacing: -0.015em;
  line-height: 1.25;
}

h1 { font-size: 1.9rem; font-weight: 640; }
h2 { font-size: 1.3rem; font-weight: 620; }
h3 { font-size: 1.08rem; font-weight: 600; }

p, li {
  line-height: 1.65;
}

a {
  color: var(--site-accent);
  text-decoration-color: color-mix(in srgb, var(--site-accent) 35%, transparent);
  text-underline-offset: 2px;
  transition: color .12s ease, text-decoration-color .12s ease;
}

a:hover {
  color: var(--site-accent-hover);
  text-decoration-color: currentColor;
}

:focus-visible {
  outline: 2px solid var(--site-accent);
  outline-offset: 2px;
  border-radius: 3px;
}

code, pre {
  font-variant-ligatures: none;
}

/* ------------------------------------------------------- declaration cards */

/* The top margin came off the heading that used to sit between the page title and the card. The
   card is now the first thing under the title and still needs the gap. */
.decl-section {
  margin-top: 1.4rem;
  scroll-margin-top: 5rem;
}

.decl-card {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-left: 3px solid var(--site-kind-definition);
  border-radius: var(--site-radius);
  box-shadow: var(--site-shadow);
  margin: 1rem 0 1.6rem;
  padding: 1rem 1.15rem;
  transition: box-shadow .16s ease, border-color .16s ease;
}

.decl-card:hover {
  box-shadow: var(--site-shadow-lift);
}

/* Keyed on the declaration's kind rather than on the card's modifier class: the modifiers only
   distinguish "headline theorem" from "definition", so a lemma fell through to the definition
   colour and read as the wrong kind of thing. */
.decl-section[data-decl-kind="Theorem"] .decl-card { border-left-color: var(--site-kind-theorem); }
.decl-section[data-decl-kind="Definition"] .decl-card,
.decl-section[data-decl-kind="Inductive"] .decl-card,
.decl-section[data-decl-kind="Opaque"] .decl-card,
.decl-section[data-decl-kind="Axiom"] .decl-card { border-left-color: var(--site-kind-definition); }
.decl-section[data-decl-kind="Instance"] .decl-card { border-left-color: var(--site-kind-instance); }
.decl-section[data-decl-kind="Structure"] .decl-card,
.decl-section[data-decl-kind="Type Class"] .decl-card { border-left-color: var(--site-kind-structure); }

/* A headline theorem — one written with `theorem`, not `lemma`, and not an instance — is the
   point of its page, so it gets a heavier rule than the machinery around it. */
.decl-card--theorem { border-left-width: 4px; }

.decl-card-header {
  align-items: flex-start;
  display: flex;
  gap: .8rem;
  justify-content: space-between;
  margin-bottom: .85rem;
}

.decl-card-title { min-width: 0; }

.decl-card-label {
  color: var(--site-ink-3);
  font-family: var(--verso-structure-font-family);
  font-size: .68rem;
  font-weight: 650;
  letter-spacing: .09em;
  text-transform: uppercase;
}

.decl-card-label--theorem {
  color: var(--site-kind-theorem);
}

.decl-card-tagbar {
  align-items: center;
  display: flex;
  flex: 0 0 auto;
  flex-wrap: wrap;
  gap: .45rem;
}

.decl-card-tags {
  display: flex;
  flex-wrap: wrap;
  gap: .4rem;
}

.decl-card-tag {
  border: 1px solid var(--site-border);
  border-radius: 999px;
  color: var(--site-ink-2);
  font-family: var(--verso-structure-font-family);
  font-size: .74rem;
  padding: .15rem .55rem;
}

.decl-card-tag.sorry {
  background: var(--site-warn-soft);
  border-color: var(--site-warn-border);
  color: var(--site-warn);
}

.decl-card-action {
  background: transparent;
  border: 1px solid var(--site-border-strong);
  border-radius: 999px;
  color: var(--site-ink-2) !important;
  font-family: var(--verso-structure-font-family);
  font-size: .76rem;
  font-weight: 550;
  padding: .25rem .7rem;
  text-decoration: none !important;
  transition: border-color .12s ease, color .12s ease, background .12s ease;
}

.decl-card-action:hover {
  background: var(--site-accent-soft);
  border-color: var(--site-accent);
  color: var(--site-accent) !important;
}

/* A `Block.details` fold. Inside a declaration card it is the proof, closing the card with a rule
   above it; standing on its own in the page flow — the `sorry` and axiom listings — it has no card
   to be placed by, so it needs room of its own or two consecutive folds read as one control. */
.site-fold { margin: .9rem 0; }

.decl-card .site-fold {
  border-top: 1px solid var(--site-border);
  margin: .9rem 0 0;
  padding-top: .7rem;
}

.decl-card summary,
details > summary {
  color: var(--site-ink-2);
  cursor: pointer;
  font-family: var(--verso-structure-font-family);
  font-size: .88rem;
  font-weight: 600;
  transition: color .12s ease;
}

.decl-card summary:hover,
details > summary:hover {
  color: var(--site-accent);
}

.decl-card details ul {
  margin: .6rem 0 0;
  padding-left: 1.2rem;
}

.decl-card details li + li { margin-top: .2rem; }

/* Code surfaces, including Verso's highlighted blocks. */
.decl-card pre,
.decl-card code.hl.lean.block,
pre.lean,
code.hl.lean.block {
  background: var(--site-surface-2) !important;
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius-sm);
  box-shadow: none;
}

.decl-card pre,
pre.lean {
  overflow-x: auto;
  padding: .8rem .95rem;
}

/* --------------------------------------------------------- prev/next nav --- */

/* Verso renders these above and below every page. They are wayfinding, not content, so they read
   as quiet secondary controls rather than competing with the page title. */
.prev-next-buttons {
  display: flex;
  gap: .6rem;
  justify-content: space-between;
  margin: .2rem 0 1.4rem;
}

.prev-next-buttons .local-button {
  align-items: baseline;
  border-radius: var(--site-radius-sm);
  color: var(--site-ink-3);
  display: inline-flex;
  font-size: .82rem;
  font-weight: 500;
  gap: .35rem;
  max-width: 45%;
  padding: .2rem .4rem;
  text-decoration: none;
  transition: background .12s ease, color .12s ease;
}

.prev-next-buttons .local-button:hover {
  background: var(--site-accent-soft);
  color: var(--site-accent);
}

.prev-next-buttons .where {
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

/* ------------------------------------------------------------- index lists */

main ul { padding-left: 1.15rem; }

main li code { font-size: .92em; }

/* ----------------------------------------------------------- sidebar tools */

.header-logo-wrapper,
.with-toc #toc,
.with-toc > main {
  transition: flex-basis var(--verso-toc-transition-time) ease,
              width var(--verso-toc-transition-time) ease,
              padding-left var(--verso-toc-transition-time) ease,
              transform var(--verso-toc-transition-time) ease;
}

.site-utility-nav {
  align-items: stretch;
  border-bottom: 1px solid var(--site-border);
  display: flex;
  flex-direction: column;
  gap: .35rem;
  margin: .2rem 0 .8rem;
  padding: 0 1rem .85rem;
}

.site-utility-link {
  border-radius: var(--site-radius-sm);
  color: var(--site-ink-2);
  font-family: var(--verso-structure-font-family);
  font-size: .84rem;
  font-weight: 550;
  padding: .2rem .35rem;
  text-decoration: none;
  transition: background .12s ease, color .12s ease;
}

.site-utility-link:hover {
  background: var(--site-accent-soft);
  color: var(--site-accent);
}

.site-utility-button {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: 999px;
  color: var(--site-ink-2);
  cursor: pointer;
  font-family: var(--verso-structure-font-family);
  font-size: .76rem;
  font-weight: 550;
  padding: .28rem .7rem;
  text-align: left;
  transition: border-color .12s ease, color .12s ease, background .12s ease;
}

.site-utility-button:hover {
  background: var(--site-accent-soft);
  border-color: var(--site-accent);
  color: var(--site-accent);
}

.site-utility-button[aria-pressed="true"] {
  background: var(--site-surface-3);
  color: var(--site-ink);
}

.site-theme-toggle {
  margin-top: .15rem;
}

/* The sidebar's visibility controls filter declaration *listings* — module contents, the claims
   and trust pages, and a declaration's dependency closures. They deliberately do not touch the
   card on a declaration's own page (which carries `data-card-group`, not `data-decl-group`):
   hiding the very thing you navigated to would be a strange thing for a filter to do. */
body.hide-definitions [data-decl-group="definition"],
body.hide-lemmas [data-decl-group="lemma"],
body.hide-theorems [data-decl-group="theorem"] {
  display: none;
}

/* With `rootTocDepth`/`sectionTocDepth` at 0 Verso still emits the wrapper for its automatic
   sub-page list, so the empty element is hidden rather than left to contribute stray margins.
   `:has` covers the case where it ever emits whitespace inside. On the landing page the list also
   comes wrapped in a `<section>` with its own "Contents" heading, which goes with it. */
.section-toc:empty,
.section-toc:not(:has(li)) {
  display: none;
}

/* Headings the site writes into page content itself (see `Block.sectionHeading`), as opposed to
   the page title Verso renders from the `Part`. */
.site-heading {
  border-top: 1px solid var(--site-border);
  margin-top: 2.2rem;
  padding-top: 1.4rem;
}

/* ------------------------------------------------------- declaration index */

.decl-index {
  list-style: none;
  margin: .6rem 0 1.2rem;
  padding: 0;
}

.decl-index-item {
  align-items: baseline;
  border-bottom: 1px solid var(--site-border);
  display: flex;
  flex-wrap: wrap;
  gap: .5rem;
  padding: .32rem .1rem;
}

.decl-index-item:last-child { border-bottom: none; }

.decl-index-item:hover { background: var(--site-surface-2); }

.decl-index-name {
  flex: 1 1 22rem;
  min-width: 0;
  overflow-wrap: anywhere;
  text-decoration: none;
}

.decl-index-name code { font-size: .9rem; }

.decl-index-meta {
  color: var(--site-ink-3);
  flex: 0 0 auto;
  font-size: .8rem;
  white-space: nowrap;
}

/* Shared with `.audit-flag` on the claims listing: the same fact about a declaration, and a reader
   moving between the two listings should not have to learn the mark twice. */
.decl-index-flag,
.audit-flag {
  background: var(--site-warn-soft);
  border: 1px solid var(--site-warn-border);
  border-radius: 999px;
  color: var(--site-warn);
  flex: 0 0 auto;
  font-size: .72rem;
  padding: .05rem .45rem;
  white-space: nowrap;
}

/* --------------------------------------------------- specification listing */

/* The theorems an author declared to be the meaning of a definition (`Block.specList`).

   Heavier than `.decl-index` on purpose. That is a list of links, scanned; this is a list of
   statements, read — each row is a property the reader has to weigh, so it gets a card of its own
   rather than a line. */

.spec-list {
  list-style: none;
  margin: .6rem 0 1.2rem;
  padding: 0;
}

.spec-item {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-left: 3px solid var(--site-kind-definition);
  border-radius: var(--site-radius-sm);
  margin-bottom: .55rem;
  padding: .6rem .8rem;
}

.spec-item:last-child { margin-bottom: 0; }

.spec-item-head {
  align-items: baseline;
  display: flex;
  flex-wrap: wrap;
  gap: .6rem;
  justify-content: space-between;
}

.spec-item-name {
  min-width: 0;
  overflow-wrap: anywhere;
  text-decoration: none;
}

.spec-item-name code { font-size: .9rem; }

.spec-item-kind {
  color: var(--site-ink-3);
  flex: 0 0 auto;
  font-family: var(--verso-structure-font-family);
  font-size: .74rem;
  white-space: nowrap;
}

/* The author's note on why the property belongs in the specification: the one part of the row
   that is prose, and the part a reader is most likely to want first. */
.spec-item-comment {
  color: var(--site-ink-2);
  font-size: .9rem;
  margin: .35rem 0 0;
}

.spec-item-statement {
  background: var(--site-surface-2);
  border-radius: var(--site-radius-sm);
  font-size: .82rem;
  margin: .45rem 0 0;
  overflow-x: auto;
  padding: .5rem .65rem;
}

.spec-item-statement code {
  font-family: var(--verso-code-font-family);
  white-space: pre;
}

/* ------------------------------------------------ characterization listing */

/* The claim that a property *determines* a definition, up to a stated relation
   (`Block.charList`). One card per claim, with the three declarations it is made of nested inside
   as ordinary `.spec-item`s.

   The banner carries the whole weight. `x = y` and `f =ᵐ[μ] g` are very different claims about how
   well a definition is pinned down, and a reader who skims the card and takes away "characterized"
   without taking away "up to what" has read it wrong — so the relation is set larger than the
   statements below it and is the first thing in the card. */

.char-list {
  list-style: none;
  margin: .6rem 0 1.2rem;
  padding: 0;
}

.char-bundle {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius);
  margin-bottom: .9rem;
  padding: .75rem .9rem .9rem;
}

.char-bundle:last-child { margin-bottom: 0; }

.char-banner {
  align-items: baseline;
  border-bottom: 1px solid var(--site-border);
  display: flex;
  flex-wrap: wrap;
  gap: .5rem .75rem;
  padding-bottom: .55rem;
}

.char-banner-label {
  color: var(--site-ok);
  font-family: var(--verso-structure-font-family);
  font-size: .74rem;
  letter-spacing: .04em;
  text-transform: uppercase;
  white-space: nowrap;
}

.char-banner-gap .char-banner-label { color: var(--site-warn); }

/* A relation nothing is known to satisfy is not reassurance, so an unfinished bundle keeps the
   warning colour even where it does have a relation to show. */
.char-banner-gap .char-relation {
  background: var(--site-warn-soft);
  border: 1px solid var(--site-warn-border);
}

.char-banner-rels {
  display: flex;
  flex-wrap: wrap;
  gap: .4rem .6rem;
  min-width: 0;
}

/* Larger than the statements below on purpose: this is the claim, they are the evidence. */
.char-relation {
  background: var(--site-ok-soft);
  border-radius: var(--site-radius-sm);
  font-family: var(--verso-code-font-family);
  font-size: 1rem;
  overflow-wrap: anywhere;
  padding: .1rem .45rem;
}

.char-relation-missing {
  color: var(--site-warn);
  font-size: .9rem;
}

.char-lede {
  color: var(--site-ink-2);
  font-size: .9rem;
  margin: .55rem 0 0;
}

.char-lede-gap { color: var(--site-warn); }

.char-lede code {
  font-family: var(--verso-code-font-family);
  overflow-wrap: anywhere;
}

/* What the relation in the banner actually says. Sits between the banner and the three parts,
   because that is where the reader asks — and it takes the banner's colour rather than the parts'
   so that it reads as the claim being spelled out, not as a fourth part of it. */
.char-relation-defs {
  list-style: none;
  margin: .55rem 0 0;
  padding: 0;
}

.char-relation-def {
  background: var(--site-surface-2);
  border-left-color: var(--site-ok);
  margin-bottom: 0;
}

.char-banner-gap ~ .char-relation-defs .char-relation-def {
  border-left-color: var(--site-warn);
}

.char-parts { margin: .55rem 0 0; }

/* The three parts read as a sequence — property, then existence, then uniqueness — so they take
   the theorem colour uniformly rather than the definition colour `.spec-item` defaults to. */
.char-part { border-left-color: var(--site-kind-theorem); }

.char-part-role {
  color: var(--site-ink-3);
  flex: 0 0 auto;
  font-family: var(--verso-structure-font-family);
  font-size: .72rem;
  letter-spacing: .04em;
  text-transform: uppercase;
  white-space: nowrap;
}

/* Repeated from the banner, for the case of several uniqueness theorems where the banner alone
   cannot say which relation belongs to which. */
.char-part-relation {
  color: var(--site-ink-2);
  font-size: .85rem;
  margin: .35rem 0 0;
}

.char-part-relation code {
  background: var(--site-surface-2);
  border-radius: var(--site-radius-sm);
  font-family: var(--verso-code-font-family);
  padding: .05rem .3rem;
}

/* ----------------------------------------------------------------- browse */

.browse-controls {
  align-items: center;
  display: flex;
  flex-wrap: wrap;
  gap: .6rem;
  margin: 1rem 0 .6rem;
}

.browse-controls input,
.browse-controls select,
.browse-controls button {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: 999px;
  color: var(--site-ink);
  font-family: var(--verso-structure-font-family);
  font-size: .85rem;
  padding: .45rem .85rem;
  transition: border-color .12s ease;
}

.browse-controls input { flex: 1 1 16rem; }
.browse-controls input::placeholder { color: var(--site-ink-3); }
.browse-controls button { cursor: pointer; }

.browse-controls input:hover,
.browse-controls select:hover,
.browse-controls button:hover { border-color: var(--site-border-strong); }

.browse-count {
  color: var(--site-ink-3);
  font-size: .84rem;
  margin: 0 0 .5rem;
}

/* The table scrolls inside its own box: a long declaration name must not widen the page. */
.browse-scroll {
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius);
  max-height: 44rem;
  overflow: auto;
}

.browse-table {
  border-collapse: collapse;
  font-size: .86rem;
  width: 100%;
}

.browse-table thead th {
  background: var(--site-surface-2);
  border-bottom: 1px solid var(--site-border);
  color: var(--site-ink-2);
  font-family: var(--verso-structure-font-family);
  font-size: .76rem;
  font-weight: 600;
  letter-spacing: .04em;
  position: sticky;
  text-align: left;
  text-transform: uppercase;
  top: 0;
  white-space: nowrap;
  z-index: 1;
}

.browse-sortable {
  cursor: pointer;
  padding: .5rem .7rem;
  user-select: none;
}

.browse-sortable:hover { color: var(--site-accent); }

/* The arrow marks which column is sorted, and which way. */
.browse-sortable[data-dir="asc"]::after { content: " ↑"; }
.browse-sortable[data-dir="desc"]::after { content: " ↓"; }
.browse-sorted { color: var(--site-ink); }

.browse-table td {
  border-bottom: 1px solid var(--site-border);
  padding: .34rem .7rem;
  vertical-align: baseline;
}

.browse-table tbody tr:last-child td { border-bottom: none; }
.browse-table tbody tr:hover { background: var(--site-surface-2); }

.browse-table td a { text-decoration: none; }
.browse-table code { font-size: .88em; overflow-wrap: anywhere; }

.browse-kind,
.browse-module { color: var(--site-ink-3); white-space: nowrap; }

.browse-num { text-align: right; white-space: nowrap; }

.browse-flag {
  border-radius: 999px;
  font-size: .72rem;
  padding: .05rem .45rem;
  white-space: nowrap;
}

.browse-flag-ok {
  background: var(--site-ok-soft);
  color: var(--site-ok);
}

.browse-flag-warn {
  background: var(--site-warn-soft);
  border: 1px solid var(--site-warn-border);
  color: var(--site-warn);
}

/* A missing specification is a gap, not a fault: the declaration may be perfectly correct and
   nobody has said what it means. Marked plainly rather than in the warning colour, which on this
   table means "depends on sorry". */
.browse-flag-gap {
  border: 1px solid var(--site-border-strong);
  color: var(--site-ink-3);
}

.browse-spec-na { color: var(--site-ink-3); }
.browse-change-na { color: var(--site-ink-3); }

/* --------------------------------------------------------------- changes --- */

/* The Changes page and the banner on a declaration whose meaning moved. Both are read by someone
   who has already worked through an earlier revision and wants to know what their reading no
   longer covers, so the visual weight follows severity: a changed statement is bordered in the
   removal colour, a proof-only change is unbordered and quiet. */

.change-list {
  display: flex;
  flex-direction: column;
  gap: .7rem;
  list-style: none;
  margin: .8rem 0 1.4rem;
  padding: 0;
}

.change-item {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-left: 3px solid var(--site-border-strong);
  border-radius: var(--site-radius-sm);
  padding: .6rem .8rem;
}

.change-item--statement,
.change-item--indirect,
.change-item--body { border-left-color: var(--site-del); }
.change-item--removed { border-left-color: var(--site-warn); }
.change-item--added { border-left-color: var(--site-ins); }
.change-item--proof,
.change-item--unchanged { border-left-color: var(--site-border-strong); }

.change-head {
  align-items: baseline;
  display: flex;
  flex-wrap: wrap;
  gap: .5rem;
}

.change-name { text-decoration: none; }
.change-name code { overflow-wrap: anywhere; }

.change-module,
.change-dependents { color: var(--site-ink-3); font-size: .8rem; }

/* Pushed to the far end of the header: it is the number that decides which of these rows to read
   first, and it should line up down the page rather than float after names of varying length. */
.change-dependents { margin-left: auto; white-space: nowrap; }

.change-chip {
  border-radius: 999px;
  font-size: .72rem;
  padding: .05rem .45rem;
  white-space: nowrap;
}

.change-chip--statement,
.change-chip--indirect,
.change-chip--upstream,
.change-chip--body {
  background: var(--site-del-soft);
  color: var(--site-del);
}

.change-chip--added {
  background: var(--site-ins-soft);
  color: var(--site-ins);
}

.change-chip--removed {
  background: var(--site-warn-soft);
  border: 1px solid var(--site-warn-border);
  color: var(--site-warn);
}

.change-chip--proof,
.change-chip--unchanged {
  border: 1px solid var(--site-border-strong);
  color: var(--site-ink-3);
}

.change-body:empty { display: none; }

.stmt-diff,
.stmt-plain {
  background: var(--site-surface-2);
  border-radius: var(--site-radius-sm);
  font-size: .82rem;
  margin: .5rem 0 0;
  overflow-x: auto;
  padding: .5rem .6rem;
  white-space: pre-wrap;
  word-break: break-word;
}

.stmt-tok--del {
  background: var(--site-del-soft);
  color: var(--site-del);
  text-decoration: line-through;
}

.stmt-tok--ins {
  background: var(--site-ins-soft);
  color: var(--site-ins);
}

.change-note {
  color: var(--site-ink-3);
  font-size: .8rem;
  margin: .4rem 0 0;
}

.change-causes-list {
  display: flex;
  flex-wrap: wrap;
  gap: .4rem;
  list-style: none;
  margin: .25rem 0 0;
  padding: 0;
}

.change-causes-list li { font-size: .82rem; }

.change-trust {
  color: var(--site-warn);
  font-size: .82rem;
  margin: .5rem 0 0;
  padding-left: 1.1rem;
}

/* The banner sits above the declaration card, so it has to read as an interruption of the page
   rather than as its first section. */
.change-banner {
  background: var(--site-surface-2);
  border: 1px solid var(--site-border);
  border-left: 3px solid var(--site-del);
  border-radius: var(--site-radius-sm);
  margin: 0 0 1rem;
  padding: .7rem .9rem;
}

.change-banner--proof,
.change-banner--unchanged { border-left-color: var(--site-border-strong); }
.change-banner--added { border-left-color: var(--site-ins); }

.change-banner-since { color: var(--site-ink-3); font-size: .8rem; }

/* The baseline's date, one step quieter than its name: the name is what a reader recognises and
   the date is the context for it, so they should not compete. Spaced with a margin rather than a
   text node, because the HTML quotation drops whitespace between adjacent inline elements. */
.change-banner-date {
  margin-left: .35rem;
  opacity: .8;
  white-space: nowrap;
}

/* ----------------------------------------------------------------- audit --- */

/* The reader's own verdicts. Styled as a control surface rather than as content: this is the one
   part of the site that is written to rather than read, and it should not look like another
   derived section. */

.audit-control {
  background: var(--site-surface-2);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius-sm);
  margin: 0 0 1.2rem;
  padding: .7rem .9rem;
}

/* Names the one box on a declaration page whose contents are the reader's rather than the
   library's. Separated by a rule so the boundary reads even when the box is scrolled past its
   own border. */
.audit-control-head {
  align-items: baseline;
  border-bottom: 1px solid var(--site-border);
  display: flex;
  gap: .5rem;
  justify-content: space-between;
  margin: -.1rem 0 .6rem;
  padding-bottom: .4rem;
}

.audit-control-title {
  color: var(--site-ink-2);
  font-size: .8rem;
  font-weight: 600;
  letter-spacing: .03em;
  text-transform: uppercase;
}

.audit-row {
  align-items: center;
  display: flex;
  flex-wrap: wrap;
  gap: .6rem;
}

.audit-verdicts {
  display: flex;
  gap: .3rem;
}

.audit-verdict {
  background: var(--site-surface);
  border: 1px solid var(--site-border-strong);
  border-radius: 999px;
  color: var(--site-ink-2);
  cursor: pointer;
  font: inherit;
  font-size: .8rem;
  padding: .15rem .7rem;
}

.audit-verdict:hover { border-color: var(--site-accent); color: var(--site-accent); }

.audit-verdict--on[data-v="accepted"] {
  background: var(--site-ok-soft);
  border-color: var(--site-ok);
  color: var(--site-ok);
}

.audit-verdict--on[data-v="query"] {
  background: var(--site-warn-soft);
  border-color: var(--site-warn-border);
  color: var(--site-warn);
}

.audit-verdict--on[data-v="unread"] {
  background: var(--site-surface-3);
  border-color: var(--site-border-strong);
  color: var(--site-ink);
}

.audit-note {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius-sm);
  color: var(--site-ink);
  font: inherit;
  font-size: .85rem;
  margin-top: .5rem;
  padding: .4rem .5rem;
  resize: vertical;
  width: 100%;
}

/* A graph with a single node and no edges. Drawn so that a declaration page keeps its shape
   whether or not anything sits under it, but given none of the room a real graph needs: there is
   no side panel to reserve width for, and 720px of empty canvas under one box reads as a broken
   picture rather than as an answer. */
.graph-layout--lone { display: block; }

/* ------------------------------------------------------------ provenance --- */

/* When a declaration last meant something else, under its card. Quiet by design: it is context for
   a reader who has already decided to look, not a warning. The change banner above the card is
   what shouts. */
.provenance-line {
  color: var(--site-ink-2);
  font-size: .85rem;
  margin: .5rem 0 0;
}

.browse-moved { white-space: nowrap; }
.browse-moved-ref { font-family: var(--site-mono); }
.browse-moved-date { color: var(--site-ink-3); font-size: .8rem; margin-left: .35rem; }

/* The revision selector on the Changes page. */
.rev-picker { align-items: baseline; display: flex; flex-wrap: wrap; gap: .5rem; margin: 1rem 0; }
.rev-picker select { font: inherit; }
.rev-result { margin: .75rem 0; }
.rev-caveat { color: var(--site-ink-3); font-size: .85rem; }

.audit-coverage,
.audit-stale,
.audit-queue {
  font-size: .85rem;
  margin: .5rem 0 0;
}

/* An acceptance of something this build no longer says. Given a border rather than colour alone:
   it is the one line in the control that reports the reader's own record as out of date, and it
   has to survive being skimmed. Collapsed when empty so the control keeps its shape. */
.audit-stale:empty { display: none; }

.audit-stale {
  background: var(--site-warn-soft);
  border-left: 3px solid var(--site-warn-border);
  border-radius: var(--site-radius-sm);
  padding: .5rem .7rem;
}

.audit-queue { color: var(--site-ink-2); }

.audit-actions {
  align-items: center;
  display: flex;
  flex-wrap: wrap;
  gap: .6rem;
  margin-top: .5rem;
}

.audit-actions button,
.audit-toolbar button {
  background: var(--site-surface);
  border: 1px solid var(--site-border-strong);
  border-radius: var(--site-radius-sm);
  color: var(--site-ink-2);
  cursor: pointer;
  font: inherit;
  font-size: .8rem;
  padding: .2rem .6rem;
}

.audit-actions button:hover,
.audit-toolbar button:hover { border-color: var(--site-accent); color: var(--site-accent); }

.audit-toolbar button.audit-danger:hover { border-color: var(--site-del); color: var(--site-del); }

.audit-ok { color: var(--site-ok); font-weight: 600; }
.audit-warn { color: var(--site-warn); font-weight: 600; }
.audit-hint { color: var(--site-ink-3); font-size: .8rem; }

.audit-link { font-size: .8rem; margin-left: auto; }

.audit-summary {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius);
  margin-bottom: 1rem;
  padding: .9rem 1.1rem;
}

/* The number that matters, and deliberately the only large one: how many claims are covered, not
   how many declarations have been ticked. */
.audit-headline {
  font-size: 1.3rem;
  font-weight: 600;
  margin: 0 0 .3rem;
}

.audit-summary p { margin: .2rem 0; }

.audit-toolbar {
  display: flex;
  flex-wrap: wrap;
  gap: .5rem;
  margin-bottom: .8rem;
}

.audit-import-note:not(:empty) {
  background: var(--site-surface-2);
  border-left: 3px solid var(--site-accent);
  border-radius: var(--site-radius-sm);
  font-size: .85rem;
  margin-bottom: 1rem;
  padding: .5rem .7rem;
}

.audit-list {
  display: flex;
  flex-direction: column;
  gap: .3rem;
  list-style: none;
  margin: .6rem 0 1.2rem;
  padding: 0;
}

.audit-item {
  align-items: baseline;
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius-sm);
  display: flex;
  flex-wrap: wrap;
  gap: .6rem;
  padding: .4rem .7rem;
  /* Anchors the docstring tooltip below. */
  position: relative;
}

.audit-name { text-decoration: none; }
.audit-name code { overflow-wrap: anywhere; }

/* The docstring, under the claim's name — the declaration's own `docBlocks`, so real paragraphs,
   code spans and math rather than a flattened string.

   `flex: 0 0 100%` is what puts it on its own line: the row is a wrapping flex line and this is its
   last item, so it takes a full line to itself under the name and the counts.

   Clamped to three lines. A docstring is prose of any length, and a listing where one claim takes
   twelve lines and the next takes one is a listing nobody can scan; three is enough to say what a
   theorem is about, and the declaration's own page has all of it. */
.audit-doc {
  /* The row aligns its items on their baselines, which for a clamped multi-line box is the *last*
     line — leaving three lines of empty space above a one-line docstring. This item is a line of
     its own, so it opts out. */
  align-self: flex-start;
  color: var(--site-ink-2);
  display: -webkit-box;
  flex: 0 0 100%;
  font-size: .85rem;
  line-height: 1.5;
  overflow: hidden;
  -webkit-box-orient: vertical;
  -webkit-line-clamp: 3;
  line-clamp: 3;
}

/* `-webkit-line-clamp` counts *line boxes*, so it only counts what it can see: a block child is one
   line however long it runs, which clamps a whole paragraph to one line and then reserves three
   lines of height for it. Making the paragraphs inline gives the clamp the text it is written for.
   A docstring of several paragraphs runs together as a result — three lines is a summary, and the
   declaration's own page is where it is read properly. */
.audit-doc p {
  display: inline;
  margin: 0;
}

.audit-doc p + p::before { content: " · "; }

.audit-doc code { font-size: .95em; }

/* A fold whose summary is a chapter heading rather than a control. Lighter than `.site-heading`,
   which separates the page's sections: these subdivide one listing, and a rule across the page at
   every chapter would break it into what looks like several pages. */
.site-fold-heading { margin: 1.4rem 0 .4rem; }

.site-fold-heading > summary {
  color: var(--site-ink-2);
  font-size: .95rem;
  letter-spacing: .01em;
}

.audit-meta { color: var(--site-ink-3); font-size: .8rem; }
.audit-note-text { color: var(--site-ink-2); font-size: .85rem; }

/* Pushed right so the buttons line up down the page rather than tracking name length. */
.audit-item .audit-start { margin-left: auto; }

/* ------------------------------------------------------------------ graph */

#graph-root {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius);
  padding: .9rem;
}

/* The view switch: which node set the picture draws. A segmented control rather than another pill
   in the toolbar, because it is a different order of choice — the toolbar narrows what you see of
   one graph, this changes which question the graph answers. */
.graph-views {
  display: flex;
  flex-wrap: wrap;
  gap: 0;
  margin-bottom: .5rem;
  width: fit-content;
}

.graph-view-btn {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  color: var(--site-ink-2);
  cursor: pointer;
  font-family: var(--verso-structure-font-family);
  font-size: .85rem;
  padding: .4rem .9rem;
  transition: background-color .12s ease, border-color .12s ease, color .12s ease;
}

.graph-view-btn + .graph-view-btn { border-left: none; }
.graph-view-btn:first-child { border-radius: 999px 0 0 999px; }
.graph-view-btn:last-child { border-radius: 0 999px 999px 0; }
.graph-view-btn:hover { border-color: var(--site-border-strong); color: var(--site-ink); }

/* The selected view. Filled rather than merely outlined: with two pills side by side an outline
   difference is not legible at a glance, and which one you are looking at is the whole point. */
.graph-view-btn[aria-pressed="true"] {
  background: var(--site-accent);
  border-color: var(--site-accent);
  color: var(--site-surface);
}

.graph-viewnote {
  color: var(--site-ink-3);
  font-size: .84rem;
  line-height: 1.55;
  margin: 0 0 .7rem;
  max-width: 62ch;
}

.graph-toolbar {
  align-items: center;
  display: flex;
  flex-wrap: wrap;
  gap: .6rem;
  margin-bottom: .7rem;
}

.graph-toolbar input,
.graph-toolbar select,
.graph-toolbar button {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: 999px;
  color: var(--site-ink);
  font-family: var(--verso-structure-font-family);
  font-size: .85rem;
  padding: .45rem .85rem;
  transition: border-color .12s ease;
}

.graph-toolbar input { flex: 1 1 18rem; }
.graph-toolbar input::placeholder { color: var(--site-ink-3); }
.graph-toolbar button { cursor: pointer; }

.graph-toolbar input:hover,
.graph-toolbar select:hover,
.graph-toolbar button:hover {
  border-color: var(--site-border-strong);
}

.graph-hint {
  color: var(--site-ink-3);
  font-size: .84rem;
  line-height: 1.55;
  margin: .2rem 0 .7rem;
}

/* The key, collapsed by default. It describes rows, arrows, transitive reduction, colours, two
   kinds of dashed outline, cycles and the verdict marks — worth having, and far too much to sit
   open above every graph on the site. */
.graph-key {
  color: var(--site-ink-3);
  font-size: .84rem;
  margin: .2rem 0 .7rem;
}

.graph-key > summary {
  cursor: pointer;
  user-select: none;
  width: fit-content;
}

.graph-key > summary:hover { color: var(--site-ink-2); }

.graph-key-list {
  display: grid;
  gap: .25rem .8rem;
  grid-template-columns: max-content minmax(0, 1fr);
  line-height: 1.5;
  margin: .5rem 0 0;
  padding-left: .2rem;
}

.graph-key-list dt {
  color: var(--site-ink-2);
  font-weight: 600;
  white-space: nowrap;
}

.graph-key-list dd { margin: 0; }

/* One column on narrow screens: the two-column grid puts a nine-word term beside a two-word
   meaning and wraps both badly. */
@media (max-width: 40rem) {
  .graph-key-list { grid-template-columns: minmax(0, 1fr); }
  .graph-key-list dd { margin: 0 0 .35rem; }
}

.graph-layout {
  display: grid;
  gap: .9rem;
  /* Wide enough for a statement to be readable, since that is now the panel's main content. */
  grid-template-columns: minmax(0, 1fr) 21rem;
}

.graph-panel {
  background: var(--site-surface-2);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius);
  padding: .85rem 1rem;
}

.graph-panel h2 {
  font-size: 1rem;
  margin-top: 0;
}

.graph-panel p { font-size: .88rem; }
.graph-panel code { font-size: .85rem; }

.graph-panel h2 {
  overflow-wrap: anywhere;
}

.graph-panel-meta {
  color: var(--site-ink-3);
  margin-top: -.4rem;
}

.graph-panel-warn {
  color: var(--site-warn);
  font-weight: 550;
}

/* A node this view stopped at. Set apart with a rule and quiet ink rather than the warning colour:
   it corrects an assumption the reader is entitled to make about the picture, which is worth
   interrupting for, but nothing here is wrong. */
.graph-panel-cut {
  border-left: 2px dotted var(--site-border-strong);
  color: var(--site-ink-2);
  line-height: 1.5;
  margin: .5rem 0;
  padding-left: .6rem;
}

/* The selected declaration's statement. Scrolls rather than wraps: a broken Lean statement is
   harder to read than one you have to nudge sideways. */
.graph-panel-code {
  background: var(--site-surface);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius-sm);
  font-family: var(--verso-code-font-family);
  font-size: .76rem;
  line-height: 1.5;
  margin: .6rem 0;
  max-height: 16rem;
  overflow: auto;
  padding: .55rem .65rem;
  white-space: pre;
}

.graph-panel-doc {
  border-left: 2px solid var(--site-border);
  color: var(--site-ink-2);
  padding-left: .6rem;
}

.graph-panel-nodoc {
  color: var(--site-ink-3);
  font-style: italic;
}

#graph-svg {
  background: var(--site-surface-2);
  border: 1px solid var(--site-border);
  border-radius: var(--site-radius-sm);
  cursor: grab;
  display: block;
}

#graph-svg:active { cursor: grabbing; }

/* Row-depth gutter labels: quiet, so they read as an axis rather than as content. */
.graph-row-label {
  fill: var(--site-ink-3);
  font-family: var(--verso-structure-font-family);
  font-size: 10px;
  letter-spacing: .08em;
  text-transform: uppercase;
  user-select: none;
}

.graph-node text.graph-label {
  font-family: var(--verso-code-font-family);
  font-size: 11.5px;
  font-weight: 550;
  pointer-events: none;
  user-select: none;
}

.graph-node rect.graph-box { transition: stroke-width .09s ease-out; }
.graph-node, #graph-svg path { transition: opacity .09s ease-out; }

/* Set by the graph script when the drawing is much wider than the column; see `graph.js`. */
.graph-layout--wide { grid-template-columns: minmax(0, 1fr); }

@media (max-width: 900px) {
  .graph-layout { grid-template-columns: 1fr; }
}

/* ------------------------------------------------------------ preferences */

@media (prefers-reduced-motion: reduce) {
  *, *::before, *::after {
    animation-duration: .001ms !important;
    transition-duration: .001ms !important;
  }
}

/* The upstream band's row labels name a package rather than a depth, so they are set apart from
   the numbered dependency rows below them. */
.graph-row-label--upstream {
  fill: var(--site-ink-2);
  text-transform: none;
  letter-spacing: .02em;
  font-style: italic;
}