/* Ice-mixing notes: one stylesheet for every page. Light and dark by
   prefers-color-scheme; no framework. */

:root {
  --bg: #fcfcfa;
  --fg: #1c1c1f;
  --muted: #5c5c66;
  --line: #d9d9dd;
  --panel: #f2f2ef;
  --link: #1a5aa8;
  --code-bg: #efefec;
  --st-proved: #1e7b34;
  --st-proved-unchecked: #6a7f12;
  --st-certified: #1f5fbf;
  --st-solver: #0e7c7c;
  --st-computed: #5a4fcf;
  --st-explored: #6e6e78;
  --st-conjecture: #8a3fa0;
  --st-open: #c25e00;
  --st-closed-route: #7a5a3a;
  --st-corrected: #9a7400;
  --st-refuted: #c0262d;
  --st-external: #9a9aa3;
  color-scheme: light dark;
}

@media (prefers-color-scheme: dark) {
  :root {
    --bg: #17171a;
    --fg: #e6e6e9;
    --muted: #a3a3ad;
    --line: #34343a;
    --panel: #212126;
    --link: #8cb8ff;
    --code-bg: #26262c;
    --st-proved: #5cc878;
    --st-proved-unchecked: #b5cc4a;
    --st-certified: #6fa3ff;
    --st-solver: #4fc4c4;
    --st-computed: #a89cff;
    --st-explored: #a9a9b3;
    --st-conjecture: #d08ae3;
    --st-open: #ffa04d;
    --st-closed-route: #c9a27a;
    --st-corrected: #e3c24a;
    --st-refuted: #ff6b70;
    --st-external: #6c6c75;
  }
}

* { box-sizing: border-box; }

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

body {
  margin: 0;
  background: var(--bg);
  color: var(--fg);
  font: 17px/1.55 Charter, "Bitstream Charter", "Iowan Old Style", Georgia, "Times New Roman", serif;
}

main, .site-nav .inner, footer.site-foot {
  max-width: 54rem;
  margin: 0 auto;
  padding: 0 16px;
}

main { padding-bottom: 3rem; }
main.wide { max-width: 72rem; }

a { color: var(--link); text-decoration-thickness: 1px; text-underline-offset: 2px; }

h1, h2, h3, h4 {
  font-family: system-ui, -apple-system, "Segoe UI", sans-serif;
  line-height: 1.25;
  margin: 1.6em 0 0.5em;
}
h1 { font-size: 1.6rem; }
h2 { font-size: 1.3rem; }
h3 { font-size: 1.1rem; }

code, pre, kbd {
  font-family: ui-monospace, "SF Mono", Menlo, Consolas, monospace;
  font-size: 0.86em;
}
code { background: var(--code-bg); padding: 0.05em 0.3em; border-radius: 3px; overflow-wrap: anywhere; }
pre { background: var(--code-bg); padding: 0.8em; overflow-x: auto; border-radius: 4px; }
pre code { background: none; padding: 0; }

table { border-collapse: collapse; width: 100%; margin: 1em 0; font-size: 0.92em; }
th, td { border-bottom: 1px solid var(--line); padding: 0.4em 0.5em; text-align: left; vertical-align: top; }
th { font-family: system-ui, -apple-system, sans-serif; font-size: 0.85em; color: var(--muted); }
.table-wrap { overflow-x: auto; }

blockquote { margin: 1em 0; padding-left: 1em; border-left: 3px solid var(--line); color: var(--muted); }

/* Site navigation */
.site-nav {
  border-bottom: 1px solid var(--line);
  background: var(--panel);
  font-family: system-ui, -apple-system, sans-serif;
  font-size: 0.92rem;
}
.site-nav .inner { display: flex; flex-wrap: wrap; gap: 0.3rem 1.1rem; padding-top: 0.6rem; padding-bottom: 0.6rem; }
.site-nav a { text-decoration: none; }
.site-nav .brand { font-weight: 600; color: var(--fg); margin-right: auto; }

footer.site-foot {
  color: var(--muted);
  font-size: 0.85rem;
  border-top: 1px solid var(--line);
  padding-top: 1rem;
  padding-bottom: 2rem;
}

/* Status badges */
.badge {
  --c: var(--st-explored);
  display: inline-block;
  font: 600 0.75rem/1.5 system-ui, -apple-system, sans-serif;
  padding: 0 0.5em;
  border-radius: 999px;
  border: 1px solid var(--c);
  color: var(--c);
  background: color-mix(in srgb, var(--c) 12%, transparent);
  white-space: nowrap;
}
.st-proved { --c: var(--st-proved); }
.st-proved-unchecked { --c: var(--st-proved-unchecked); }
.st-certified { --c: var(--st-certified); }
.st-solver { --c: var(--st-solver); }
.st-computed { --c: var(--st-computed); }
.st-explored { --c: var(--st-explored); }
.st-conjecture { --c: var(--st-conjecture); }
.st-open { --c: var(--st-open); }
.st-closed-route { --c: var(--st-closed-route); }
.st-corrected { --c: var(--st-corrected); }
.st-refuted { --c: var(--st-refuted); }
.st-external { --c: var(--st-external); }

.kind { font: 0.8rem system-ui, sans-serif; color: var(--muted); }
.muted { color: var(--muted); }
.small { font-size: 0.88em; }

/* Panels */
.panel {
  background: var(--panel);
  border: 1px solid var(--line);
  border-radius: 6px;
  padding: 0.8rem 1rem;
  margin: 1.2rem 0;
}
.panel h2, .panel h3 { margin-top: 0.2em; }
.panel.open-problems { border-left: 4px solid var(--st-open); }

dl.fields { display: grid; grid-template-columns: max-content 1fr; gap: 0.4rem 1rem; margin: 1rem 0; }
dl.fields dt { font: 600 0.85rem/1.8 system-ui, sans-serif; color: var(--muted); }
dl.fields dd { margin: 0; min-width: 0; }
@media (max-width: 600px) {
  dl.fields { grid-template-columns: 1fr; gap: 0.1rem; }
  dl.fields dd { margin-bottom: 0.6rem; }
}

.statement {
  border-left: 4px solid var(--c, var(--line));
  padding: 0.2rem 0 0.2rem 1rem;
  margin: 1rem 0;
  font-size: 1.05em;
}

ul.plain { list-style: none; padding-left: 0; }
ul.plain li { margin: 0.3em 0; }

.hash { font-family: ui-monospace, Menlo, monospace; font-size: 0.78em; overflow-wrap: anywhere; color: var(--muted); }

/* Claims table filters */
.filters { display: flex; flex-wrap: wrap; gap: 0.6rem 1rem; align-items: end; font: 0.9rem system-ui, sans-serif; }
.filters label { display: flex; flex-direction: column; gap: 0.2rem; color: var(--muted); }
.filters select, .filters input {
  font: inherit; color: var(--fg); background: var(--bg);
  border: 1px solid var(--line); border-radius: 4px; padding: 0.3rem 0.4rem; min-width: 10rem;
}
#claim-count { color: var(--muted); }
table.claims td .muted { margin-top: 0.15em; }
.gist { font-size: 1.05rem; color: var(--muted); margin-top: -0.4rem; }
table.claims td.id { font-family: ui-monospace, Menlo, monospace; font-size: 0.8em; overflow-wrap: anywhere; }
@media (max-width: 700px) {
  table.claims .opt { display: none; }
}

/* Legend */
.legend { display: flex; flex-wrap: wrap; gap: 0.4rem 0.8rem; margin: 0.8rem 0; }
dl.vocab dt { margin-top: 0.6em; }
dl.vocab dd { margin-left: 0; }

/* Graph */
#graph {
  width: 100%;
  height: 75vh;
  min-height: 420px;
  border: 1px solid var(--line);
  border-radius: 6px;
  background: var(--bg);
  touch-action: none;
}
#graph text { font: 11px system-ui, sans-serif; fill: var(--fg); pointer-events: none; }
#graph .node { cursor: pointer; }
#graph .edge { stroke: var(--muted); stroke-opacity: 0.55; fill: none; }
#graph .edge.supersedes { stroke-dasharray: 4 3; }

/* Pandoc documents */
.doc-head .title { margin-bottom: 0.3em; }
.doc-head .subtitle { font-size: 1.1em; color: var(--muted); margin-top: 0; }
.doc-head .author, .doc-head .date { color: var(--muted); margin: 0.2em 0; }
.abstract { background: var(--panel); border-radius: 6px; padding: 0.6rem 1rem; margin: 1rem 0; }
.abstract h2 { font-size: 1rem; margin-top: 0.4em; }
nav.toc { font-size: 0.92em; margin: 1rem 0; }
nav.toc summary { cursor: pointer; font-family: system-ui, sans-serif; color: var(--muted); }
nav.toc ul { padding-left: 1.2em; }
.doc img { max-width: 100%; height: auto; }
.math.display { display: block; overflow-x: auto; overflow-y: hidden; }
mjx-container[display="true"] { overflow-x: auto; overflow-y: hidden; }
#refs .csl-entry { margin: 0.4em 0; padding-left: 1.5em; text-indent: -1.5em; }