/* Lean-QIT Catalog
   A reference instrument, not a landing page. Dense, quiet, typographic.
   No framework, no build step -- this file is served as written. */

/* The font stack is load-bearing. Signatures use 238 distinct characters,
   146 of them non-ASCII: ℝ ℕ ℂ ⊗ ⨆ ⦃⦄ ᴴ 𝔼 and so on. A stack that falls
   through to a font without this coverage renders tofu boxes in every
   signature, which is instantly disqualifying for this audience.
   JuliaMono and Iosevka both have full Lean coverage. DejaVu Sans Mono is
   the fallback that ships almost everywhere and covers most of the range.

   The @font-face rule for a self-hosted subset lives in font.css, which the
   build writes only when the woff2 is actually present -- declaring it
   unconditionally would 404 on every page load for everyone who has not run
   `make font`. See tools/subset_font.py. */

:root {
  color-scheme: light;
  --mono: "JuliaMono", "Iosevka", "JetBrains Mono", "Cascadia Code",
          "DejaVu Sans Mono", "Menlo", "Consolas", monospace;
  --sans: ui-sans-serif, -apple-system, "Segoe UI", Inter, Roboto,
          "Helvetica Neue", sans-serif;

  --bg:        #fbfbfa;
  --bg-raised: #ffffff;
  --bg-sunken: #f2f2f0;
  --ink:       #16171a;
  --ink-2:     #4a4d55;
  --ink-3:     #63666e;   /* 4.5:1+ on --bg; was #7c8089 at 3.8:1 */
  --rule:      #e2e2de;
  --rule-2:    #d0d0cb;
  --accent:    #1d4ed8;
  --accent-bg: #eaf0ff;

  --k-theorem:     #1a6a4a;
  --k-definition:  #2c5aa8;
  --k-structure:   #8a4b17;
  --k-instance:    #7a3a86;
  --k-constructor: #6a6a2a;
  --k-inductive:   #a03a3a;

  --warn:      #9a5b00;
  --warn-bg:   #fdf3e2;
  --ok:        #1a6a4a;

  --row-h: 33px;
  --pad: 15px;
  --radius: 5px;
}

:root[data-theme="dark"] {
  color-scheme: dark;
  --bg:        #131417;
  --bg-raised: #191b1f;
  --bg-sunken: #0e0f12;
  --ink:       #e6e7ea;
  --ink-2:     #a8abb4;
  --ink-3:     #8d9099;   /* 4.5:1+ on --bg; was #74777f at 4.1:1 */
  --rule:      #292b31;
  --rule-2:    #383b43;
  --accent:    #7aa2f7;
  --accent-bg: #1b2540;

  --k-theorem:     #6cc39a;
  --k-definition:  #7aa2f7;
  --k-structure:   #d99a5c;
  --k-instance:    #c99ad4;
  --k-constructor: #bcbc7a;
  --k-inductive:   #e08a8a;

  --warn:      #d9a441;
  --warn-bg:   #2b2317;
  --ok:        #6cc39a;
}

:root[data-density="compact"] { --row-h: 26px; --pad: 10px; }

* { box-sizing: border-box; }

/* Scrollbars, themed. `color-scheme` above already hands the browser the right
   palette; these rules just make them quieter and match the rule colour. */
* { scrollbar-color: var(--rule-2) transparent; scrollbar-width: thin; }
::-webkit-scrollbar { width: 12px; height: 12px; }
::-webkit-scrollbar-track { background: var(--bg-sunken); }
::-webkit-scrollbar-thumb {
  background: var(--rule-2); border-radius: 7px;
  border: 3px solid var(--bg-sunken);
}
::-webkit-scrollbar-thumb:hover { background: var(--ink-3); }
::-webkit-scrollbar-corner { background: var(--bg-sunken); }

html { -webkit-text-size-adjust: 100%; }

body {
  margin: 0;
  background: var(--bg);
  color: var(--ink);
  font: 15.5px/1.55 var(--sans);
  font-variant-numeric: tabular-nums;
  overflow-y: scroll; /* reserve the scrollbar: zero layout shift on route change */
}

a { color: var(--accent); text-decoration: none; }
a:hover { text-decoration: underline; }

code, .mono, pre { font-family: var(--mono); font-size: 14px; }

button, input, select {
  font: inherit; color: inherit;
  background: var(--bg-raised);
  border: 1px solid var(--rule-2);
  border-radius: var(--radius);
  padding: 4px 8px;
}
button { cursor: pointer; }
button:hover { border-color: var(--ink-3); }
button:focus-visible, input:focus-visible, a:focus-visible {
  outline: 2px solid var(--accent); outline-offset: 1px;
}

/* Route changes move focus to the page heading so screen readers announce the
   new page. The heading is only focusable programmatically, and Chrome draws
   its default ring on it, which put a box around the title of every
   declaration page for mouse users. Suppress the ring for programmatic focus,
   keep it for anyone who actually tabbed there. */
[tabindex="-1"]:focus { outline: none; }
[tabindex="-1"][data-kbd]:focus { outline: 2px solid var(--accent); outline-offset: 2px; }

/* ---------- shell ---------- */

.topbar {
  position: sticky; top: 0; z-index: 50;
  display: flex; align-items: center; gap: 12px;
  padding: 8px 16px;
  background: var(--bg-raised);
  border-bottom: 1px solid var(--rule);
  flex-wrap: wrap;
}
.tools { display: flex; gap: 4px; margin-left: auto; }

/* Visible only to assistive technology. */
.visually-hidden {
  position: absolute; width: 1px; height: 1px;
  margin: -1px; padding: 0; border: 0;
  clip: rect(0 0 0 0); clip-path: inset(50%); overflow: hidden;
  white-space: nowrap;
}

.skiplink {
  position: absolute; left: 8px; top: -60px; z-index: 100;
  background: var(--bg-raised); color: var(--accent);
  border: 1px solid var(--accent); border-radius: var(--radius);
  padding: 7px 12px; font-size: 14px;
  transition: top 0.12s ease;
}
.skiplink:focus { top: 8px; }

.brand {
  font-weight: 640; letter-spacing: -0.01em;
  color: var(--ink); white-space: nowrap;
}
.brand .bthin { font-weight: 640; color: var(--ink); }
.brand small {
  display: block; font-weight: 400; font-size: 11.5px;
  color: var(--ink-3); letter-spacing: 0.02em;
}

.searchwrap { position: relative; flex: 1; max-width: 720px; }
#q {
  width: 100%; padding: 6px 84px 6px 30px;
  font-family: var(--mono); font-size: 14.5px;
  background: var(--bg-sunken); border: 1px solid var(--rule-2);
}
#q::placeholder { color: var(--ink-3); font-family: var(--sans); }
.searchwrap .icon {
  position: absolute; left: 9px; top: 50%; transform: translateY(-50%);
  color: var(--ink-3); pointer-events: none; font-size: 13px;
}
.searchwrap .hint {
  position: absolute; right: 8px; top: 50%; transform: translateY(-50%);
  color: var(--ink-3); font-size: 11.5px; pointer-events: none;
}
.searchwrap .hint kbd {
  font-family: var(--mono); border: 1px solid var(--rule-2);
  border-radius: 3px; padding: 0 4px; background: var(--bg-raised);
}

.topnav { display: flex; gap: 2px; }
.topnav a {
  padding: 4px 9px; border-radius: var(--radius);
  color: var(--ink-2); font-size: 14px; white-space: nowrap;
}
.topnav a:hover { background: var(--bg-sunken); text-decoration: none; }
.topnav a.on { background: var(--accent-bg); color: var(--accent); }

.iconbtn { padding: 4px 7px; font-size: 13px; line-height: 1.2; }
a.linkbtn {
  border: 1px solid var(--rule-2); border-radius: var(--radius);
  padding: 4px 7px; font-size: 13px; background: var(--bg-raised);
}
a.linkbtn:hover { border-color: var(--ink-3); text-decoration: none; }

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

.layout {
  display: grid;
  grid-template-columns: 250px minmax(0, 1fr);
  gap: 0;
  align-items: start;
  max-width: 1500px; margin: 0 auto;
}
.sidebar {
  position: sticky; top: 45px;
  height: calc(100vh - 45px);
  overflow-y: auto;
  border-right: 1px solid var(--rule);
  padding: var(--pad);
}
.main { padding: var(--pad) 20px 80px; min-width: 0; }

/* ---------- narrow screens ----------
   The nav used to be display:none below 900px with nothing in its place, so
   every section of the site was unreachable on a phone. It now wraps onto its
   own full-width row and scrolls horizontally if it has to, which needs no
   JavaScript and no hamburger. */

@media (max-width: 900px) {
  .layout { grid-template-columns: 1fr; }
  .sidebar { position: static; height: auto; border-right: 0;
             border-bottom: 1px solid var(--rule); }
  .topbar { padding: 8px 12px; gap: 8px; row-gap: 6px; }
  .brand { flex: 1 1 auto; font-size: 14.5px; }
  .brand small { font-size: 10.5px; }
  .searchwrap { order: 3; flex: 1 0 100%; max-width: none; }
  .topnav {
    order: 4; flex: 1 0 100%;
    overflow-x: auto; -webkit-overflow-scrolling: touch;
    scrollbar-width: none;
    padding-bottom: 2px;
  }
  .topnav::-webkit-scrollbar { display: none; }
  .topnav a { padding: 5px 10px; font-size: 14.5px; }
  .searchwrap .hint { display: none; }
  #q { padding-right: 12px; }
  .main { padding: var(--pad) 12px 60px; }
  .sidebar { padding: 10px 12px; }
  /* Long Lean names and signatures must wrap rather than push the page wide. */
  .declhead h1 { font-size: 16.5px; overflow-wrap: anywhere; }
  pre.sig { font-size: 13px; }
  .reflist a, .reflist span { overflow-wrap: anywhere; max-width: 100%; }
  .row { gap: 6px; }
  .row .mod { display: none; }
  .cards { grid-template-columns: repeat(auto-fill, minmax(140px, 1fr)); }
  table { font-size: 13px; }
  th, td { padding: 4px 5px; }
  .doc pre, .doc code, code { overflow-wrap: anywhere; }
}

@media (max-width: 460px) {
  .row .deg { display: none; }
  .brand small { display: none; }
}

@media (prefers-reduced-motion: reduce) {
  * { animation-duration: 0.01ms !important; transition-duration: 0.01ms !important; }
}

/* ---------- facets ---------- */

.facet { margin-bottom: 16px; }
.facet h3 {
  margin: 0 0 5px; font-size: 11.5px; font-weight: 620;
  text-transform: uppercase; letter-spacing: 0.07em; color: var(--ink-3);
}
.facet label {
  display: flex; align-items: center; gap: 6px;
  padding: 2px 4px; border-radius: 3px; cursor: pointer; font-size: 14px;
}
.facet label:hover { background: var(--bg-sunken); }
.facet input[type=checkbox], .facet input[type=radio] { margin: 0; accent-color: var(--accent); }
.facet .n { margin-left: auto; color: var(--ink-3); font-size: 12px; font-family: var(--mono); }
.facet select { width: 100%; }

.clearbtn { width: 100%; margin-top: 4px; font-size: 13px; color: var(--ink-2); }

/* ---------- result list ---------- */

.resulthead {
  display: flex; align-items: baseline; gap: 10px;
  padding-bottom: 6px; margin-bottom: 4px;
  border-bottom: 1px solid var(--rule);
  flex-wrap: wrap;
}
.resulthead .count { font-size: 14.5px; color: var(--ink-2); }
.resulthead .count b { color: var(--ink); font-variant-numeric: tabular-nums; }
.resulthead .spacer { flex: 1; }
.resulthead label { font-size: 13px; color: var(--ink-3); }

#viewport { position: relative; }
#spacer { position: relative; width: 100%; }
#rows { position: absolute; top: 0; left: 0; right: 0; }

.row {
  display: flex; align-items: center; gap: 8px;
  height: var(--row-h); padding: 0 6px;
  border-bottom: 1px solid var(--rule);
  white-space: nowrap; overflow: hidden;
}
.row:hover { background: var(--bg-sunken); }
.row.sel { background: var(--accent-bg); box-shadow: inset 2px 0 0 var(--accent); }
.row .nm {
  font-family: var(--mono); font-size: 14px;
  overflow: hidden; text-overflow: ellipsis; flex: 1; min-width: 0;
}
.row .nm .ns { color: var(--ink-3); }
.row .nm mark { background: var(--accent-bg); color: inherit; border-radius: 2px; }
.row .mod {
  font-family: var(--mono); font-size: 12px; color: var(--ink-3);
  max-width: 34%; overflow: hidden; text-overflow: ellipsis; direction: rtl; text-align: right;
}
.row .deg {
  font-family: var(--mono); font-size: 12px; color: var(--ink-3);
  min-width: 44px; text-align: right;
}
.row .nodoc { color: var(--warn); font-size: 12px; }

.kind {
  font-size: 11px; font-weight: 640; letter-spacing: 0.04em;
  text-transform: uppercase; min-width: 34px;
}
.kind.theorem     { color: var(--k-theorem); }
.kind.definition  { color: var(--k-definition); }
.kind.structure   { color: var(--k-structure); }
.kind.instance    { color: var(--k-instance); }
.kind.constructor { color: var(--k-constructor); }
.kind.inductive   { color: var(--k-inductive); }

.empty { padding: 40px 10px; color: var(--ink-3); text-align: center; }
.empty code { color: var(--ink-2); }

/* ---------- declaration page ---------- */

.declhead { border-bottom: 1px solid var(--rule); padding-bottom: 10px; margin-bottom: 14px; }
.declhead .crumb { font-size: 12.5px; color: var(--ink-3); margin-bottom: 5px; font-family: var(--mono); }
.declhead h1 {
  margin: 0; font-family: var(--mono); font-size: 18.5px; font-weight: 600;
  line-height: 1.35; word-break: break-word;
}
.declhead h1 .ns { color: var(--ink-3); font-weight: 400; }
.declmeta {
  display: flex; flex-wrap: wrap; gap: 6px 14px; margin-top: 8px;
  font-size: 13px; color: var(--ink-2); align-items: center;
}

.chip {
  display: inline-block; padding: 1px 7px; border-radius: 10px;
  background: var(--bg-sunken); border: 1px solid var(--rule);
  font-size: 12px; color: var(--ink-2);
}
.chip.attr { font-family: var(--mono); color: var(--k-instance); }
.chip.warnchip { background: var(--warn-bg); border-color: var(--warn); color: var(--warn); }

section.block { margin: 0 0 20px; }
section.block > h2 {
  font-size: 11.5px; font-weight: 620; text-transform: uppercase;
  letter-spacing: 0.07em; color: var(--ink-3);
  margin: 0 0 6px; padding-bottom: 3px; border-bottom: 1px solid var(--rule);
  display: flex; align-items: center; gap: 8px;
}
section.block > h2 .n { color: var(--ink-3); font-family: var(--mono); font-weight: 400; }
section.block > h2 .spacer { flex: 1; }

pre.sig {
  margin: 0; padding: 11px 13px;
  background: var(--bg-raised); border: 1px solid var(--rule);
  border-radius: var(--radius);
  white-space: pre-wrap; word-break: break-word;
  line-height: 1.65; font-size: 14px; overflow-x: auto;
}
.sig .imp  { color: var(--ink-3); }
.sig .kw   { color: var(--k-instance); }
.sig .num  { color: var(--k-structure); }
.sig .op   { color: var(--ink-2); }

.doc { line-height: 1.62; color: var(--ink); max-width: 76ch; }
.doc p { margin: 0 0 9px; }
.doc code {
  background: var(--bg-sunken); border: 1px solid var(--rule);
  border-radius: 3px; padding: 0.5px 4px;
}
.doc pre {
  background: var(--bg-sunken); border: 1px solid var(--rule);
  border-radius: var(--radius); padding: 9px 11px; overflow-x: auto;
}
.doc pre code { background: none; border: 0; padding: 0; }
.doc ul, .doc ol { margin: 0 0 9px; padding-left: 22px; }
.doc .nodoc { color: var(--ink-3); font-style: italic; }

.reflist { display: flex; flex-wrap: wrap; gap: 3px 5px; }
.reflist a, .reflist span {
  font-family: var(--mono); font-size: 12.5px;
  padding: 1px 6px; border-radius: 3px;
  background: var(--bg-sunken); border: 1px solid var(--rule);
}
.reflist span.ext { color: var(--ink-3); }

.hubnote {
  background: var(--warn-bg); border: 1px solid var(--rule-2);
  border-left: 3px solid var(--warn);
  border-radius: var(--radius); padding: 9px 12px; margin-bottom: 8px;
  font-size: 14px; color: var(--ink-2);
}
.modgroup { border-bottom: 1px solid var(--rule); }
.modgroup > summary {
  cursor: pointer; padding: 4px 2px; font-family: var(--mono); font-size: 13px;
  display: flex; gap: 8px; align-items: center;
}
.modgroup > summary:hover { background: var(--bg-sunken); }
.modgroup > summary .n { margin-left: auto; color: var(--ink-3); font-size: 12px; }
.modgroup .reflist { padding: 5px 2px 9px 16px; }

.caveat {
  font-size: 12.5px; color: var(--ink-3); line-height: 1.5;
  margin-top: 6px; max-width: 76ch;
}

.sourcebar {
  display: flex; flex-wrap: wrap; gap: 6px; margin-top: 4px;
}

/* ---------- tables / stats ---------- */

table { border-collapse: collapse; width: 100%; font-size: 14px; }
th, td { text-align: left; padding: 4px 8px; border-bottom: 1px solid var(--rule); }
th { color: var(--ink-3); font-weight: 620; font-size: 11.5px;
     text-transform: uppercase; letter-spacing: 0.06em; }
td.num, th.num { text-align: right; font-family: var(--mono); }
td.mono { font-family: var(--mono); font-size: 12.5px; }

.cards { display: grid; grid-template-columns: repeat(auto-fill, minmax(160px, 1fr)); gap: 10px; }
.card {
  background: var(--bg-raised); border: 1px solid var(--rule);
  border-radius: var(--radius); padding: 11px 13px;
}
.card .v { font-size: 24px; font-weight: 620; letter-spacing: -0.02em; font-variant-numeric: tabular-nums; }
.card .l { font-size: 12px; color: var(--ink-3); margin-top: 1px; }
.card .s { font-size: 12px; color: var(--ink-2); margin-top: 5px; }

.bar {
  display: block; height: 5px; background: var(--bg-sunken);
  border-radius: 3px; overflow: hidden; min-width: 40px;
}
.bar i { display: block; height: 100%; background: var(--accent); }

/* ---------- trees ---------- */

.tree { font-family: var(--mono); font-size: 14px; }
.tree details > summary {
  cursor: pointer; padding: 2px 4px; border-radius: 3px;
  display: flex; align-items: center; gap: 7px;
}
.tree details > summary:hover { background: var(--bg-sunken); }
.tree .n { margin-left: auto; color: var(--ink-3); font-size: 12px; }
.tree .kids { margin-left: 13px; border-left: 1px solid var(--rule); padding-left: 7px; }
.tree a.leaf { display: flex; gap: 7px; padding: 2px 4px; border-radius: 3px; color: var(--ink); }
.tree a.leaf:hover { background: var(--bg-sunken); text-decoration: none; }

/* ---------- modules page ---------- */

.filterbar {
  display: flex; align-items: center; gap: 10px;
  margin-bottom: 10px; flex-wrap: wrap;
}
.filterbar input {
  flex: 1; min-width: 200px; max-width: 420px;
  font-family: var(--mono); font-size: 14px;
  background: var(--bg-sunken);
}
.filterbar .caveat { margin-top: 0; }

.areagroup { border: 1px solid var(--rule); border-radius: var(--radius);
             background: var(--bg-raised); margin-bottom: 7px; }
.areagroup > summary {
  cursor: pointer; padding: 8px 12px;
  display: flex; align-items: center; gap: 12px;
  border-radius: var(--radius); list-style: none;
}
.areagroup > summary::-webkit-details-marker { display: none; }
.areagroup > summary::before {
  content: "\25B8"; color: var(--ink-3); font-size: 11px;
  transition: transform 0.12s ease; display: inline-block;
}
.areagroup[open] > summary::before { transform: rotate(90deg); }
.areagroup > summary:hover { background: var(--bg-sunken); }
.areagroup > summary:focus-visible { outline: 2px solid var(--accent); outline-offset: -2px; }
.areagroup .aname { font-weight: 620; font-size: 14.5px; }
.areagroup .amods { color: var(--ink-3); font-size: 12.5px; }
.areagroup > summary .n {
  margin-left: auto; font-family: var(--mono); font-size: 13px; color: var(--ink-2);
}
.areagroup .bar.mini { width: 70px; flex: none; }

.modtable { border-top: 1px solid var(--rule); }
.modtable th { padding-top: 7px; }
.modtable td, .modtable th { padding-left: 12px; }
.modtable tr:last-child td { border-bottom: 0; }

/* ---------- site footer ----------
   Present on every page, not only About. Declaration pages are where search
   results land, and they are full of text written by the Lean-QIT authors, so
   that is precisely where the attribution has to be visible. */

.sitefoot {
  margin-top: 52px; padding-top: 18px;
  border-top: 1px solid var(--rule);
  font-size: 12.5px; color: var(--ink-2); line-height: 1.6;
}
.sitefoot p { margin: 0 0 7px; }
.sitefoot b { color: var(--ink); }
.sitefoot .machine { color: var(--ink-3); margin-top: 14px; }
.sitefoot .small { color: var(--ink-3); }
.footgrid {
  display: grid; gap: 20px 34px;
  grid-template-columns: repeat(auto-fit, minmax(230px, 1fr));
  max-width: 1100px;
}
.footgrid h4 {
  margin: 0 0 6px; font-size: 11px; font-weight: 620;
  text-transform: uppercase; letter-spacing: 0.07em; color: var(--ink-3);
}
.footlinks { list-style: none; margin: 0 0 7px; padding: 0; }
.footlinks li { margin-bottom: 3px; }
/* The stable-URL line carries a full Lean name, which can be 90 characters.
   Without this it is one unbreakable token and pushes the page wide. */
.sitefoot code, .caveat code, .notice code { overflow-wrap: anywhere; }

.notice {
  background: var(--bg-raised); border: 1px solid var(--rule);
  border-left: 3px solid var(--accent);
  border-radius: var(--radius); padding: 11px 14px; margin-bottom: 16px;
  font-size: 14px; color: var(--ink-2); line-height: 1.6; max-width: 88ch;
}
.notice b { color: var(--ink); }
.notice.small { padding: 8px 11px; font-size: 13px; margin-bottom: 12px; }
.notice.small a { margin-right: 8px; }

.copied { color: var(--ok); font-size: 12px; }

.foot {
  margin-top: 40px; padding-top: 12px; border-top: 1px solid var(--rule);
  font-size: 12.5px; color: var(--ink-3); line-height: 1.6;
}

.skeleton { color: var(--ink-3); padding: 20px 4px; font-size: 14px; }