/* Halmos — a reading surface for mathematics.
 *
 * Design brief: this is a text site whose content is often a formula, so the
 * page gets out of the way. Paper ground, one accent, dense enough to scan a
 * front page in a glance. The ∎ mark is the only ornament and it is never
 * decorative — it appears exactly where a kernel accepted a proof.
 */

:root {
  --paper:      #f7f6f3;
  --card:       #fffefb;
  --ink:        #1a1a17;
  --ink-soft:   #4a4943;
  --muted:      #6f6e66;
  --rule:       #e2e0d8;
  --accent:     #2f5d8a;
  --accent-dim: #eaf0f6;
  --proved:     #14663f;
  --proved-bg:  #e8f3ed;
  --refuted:    #9d2a2f;
  --refuted-bg: #f7eaea;
  --warn:       #8a6210;
  --warn-bg:    #f8f1e0;
  --mono: ui-monospace, "SF Mono", "JetBrains Mono", Menlo, Consolas, monospace;
  --serif: "Iowan Old Style", "Palatino Linotype", Palatino, Georgia, serif;
}

@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --paper: #14150f; --card: #191a13; --ink: #e9e7dd; --ink-soft: #c3c1b6;
    --muted: #8d8b80; --rule: #2c2d24; --accent: #86b3dd; --accent-dim: #1b2530;
    --proved: #5fc79b; --proved-bg: #12261e; --refuted: #e08b8e; --refuted-bg: #2a1616;
    --warn: #d7ab5b; --warn-bg: #2a2213;
  }
}

* { box-sizing: border-box; }

body {
  margin: 0;
  background: var(--paper);
  color: var(--ink);
  font: 15px/1.55 -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica, Arial, sans-serif;
  -webkit-text-size-adjust: 100%;
}

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

.wrap { max-width: 860px; margin: 0 auto; padding: 0 16px; }

/* --- masthead ---------------------------------------------------------- */

.masthead { border-bottom: 1px solid var(--rule); background: var(--card); }
.masthead .wrap { display: flex; align-items: baseline; gap: 18px; padding: 12px 16px; flex-wrap: wrap; }
.brand {
  font: 600 20px/1 var(--serif);
  color: var(--ink); letter-spacing: -0.01em; white-space: nowrap;
}
.brand:hover { text-decoration: none; }
.brand .qed { color: var(--proved); }
.masthead nav { display: flex; gap: 14px; flex: 1 1 auto; flex-wrap: wrap; }
.masthead nav a { color: var(--ink-soft); font-size: 13.5px; }
.masthead nav a.on { color: var(--ink); font-weight: 600; }
.masthead .me { font-size: 13px; color: var(--muted); white-space: nowrap; }

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

.items { list-style: none; margin: 0; padding: 14px 0; counter-reset: rank; }
.item { display: flex; gap: 8px; padding: 7px 0; align-items: baseline; }
.item .n { counter-increment: rank; color: var(--muted); font-size: 13px;
           min-width: 2.1em; text-align: right; font-variant-numeric: tabular-nums; }
.item .n::after { content: counter(rank) "."; }

.vote {
  background: none; border: 0; padding: 0 2px; cursor: pointer;
  color: var(--muted); font-size: 13px; line-height: 1;
}
.vote:hover { color: var(--accent); }
.vote[disabled] { color: var(--accent); cursor: default; opacity: .85; }

.item .main { flex: 1 1 auto; min-width: 0; }
.item .t { font-size: 15.5px; color: var(--ink); }
.item .t:hover { color: var(--accent); }
.item .host { color: var(--muted); font-size: 12.5px; }
.item .meta { color: var(--muted); font-size: 12.5px; margin-top: 2px; }
.item .meta a { color: var(--muted); }
.item .meta a:hover { color: var(--accent); }

/* --- the mark ---------------------------------------------------------- */
/* `∎` is reserved. It renders only where a kernel accepted a proof with no
 * `sorry`, no new axiom and no skipped type-checking. Everything else gets a
 * word, never the mark — the whole value is that it cannot be talked into
 * existence, so it must not be handed out for "the tool ran". */

.tag {
  display: inline-block; font: 600 11px/1.6 var(--mono);
  padding: 0 6px; border-radius: 3px; vertical-align: 1px;
  border: 1px solid transparent; white-space: nowrap;
}
.tag-proved  { color: var(--proved);  background: var(--proved-bg);  border-color: var(--proved); }
.tag-refuted { color: var(--refuted); background: var(--refuted-bg); }
.tag-assumed { color: var(--warn);    background: var(--warn-bg); }
.tag-stale   { color: var(--warn);    background: var(--warn-bg); }
.tag-ran     { color: var(--muted);   background: var(--accent-dim); }
.tag-running,
.tag-queued  { color: var(--muted);   background: transparent; border-color: var(--rule); }
.tag-error   { color: var(--refuted); background: transparent; border-color: var(--rule); }

/* --- content ----------------------------------------------------------- */

.post { padding: 16px 0 4px; border-bottom: 1px solid var(--rule); }
.post h1 { font: 600 22px/1.3 var(--serif); margin: 0 0 6px; }
.body { font-size: 15px; color: var(--ink-soft); overflow-wrap: break-word; }
.body p { margin: 0 0 .85em; }
.body pre {
  background: var(--card); border: 1px solid var(--rule); border-radius: 4px;
  padding: 10px 12px; overflow-x: auto; font: 13px/1.5 var(--mono); margin: 0;
}
.body code { font: 13px/1.4 var(--mono); }
.body :not(pre) > code { background: var(--accent-dim); padding: 1px 4px; border-radius: 3px; }
.body blockquote {
  margin: 0 0 .85em; padding-left: 12px; border-left: 2px solid var(--rule); color: var(--muted);
}
.body table { border-collapse: collapse; width: 100%; display: block; overflow-x: auto; }
.body th, .body td { border: 1px solid var(--rule); padding: 4px 8px; text-align: left; }

/* --- a runnable block and its receipt ---------------------------------- */

figure.run { margin: 0 0 1em; border: 1px solid var(--rule); border-radius: 5px; overflow: hidden; }
figure.run figcaption {
  font: 600 11px/1 var(--mono); text-transform: uppercase; letter-spacing: .06em;
  color: var(--muted); background: var(--accent-dim); padding: 6px 10px;
  border-bottom: 1px solid var(--rule);
}
figure.run pre { border: 0; border-radius: 0; background: var(--card); }
.run-out { border-top: 1px solid var(--rule); padding: 7px 10px; font-size: 12.5px; }
.run-badge { font: 600 11.5px/1.6 var(--mono); }
.run-ms { color: var(--muted); font: 11px/1.6 var(--mono); margin-left: 8px; }
.run-output {
  margin: 6px 0 0; background: transparent; border: 0; padding: 0;
  color: var(--ink-soft); max-height: 22em; overflow: auto; white-space: pre-wrap;
}
.run-proved  { background: var(--proved-bg); }
.run-proved  .run-badge { color: var(--proved); }
.run-refuted { background: var(--refuted-bg); }
.run-refuted .run-badge { color: var(--refuted); }
.run-assumed, .run-stale { background: var(--warn-bg); }
.run-assumed .run-badge, .run-stale .run-badge { color: var(--warn); }
.run-error .run-badge { color: var(--refuted); }
.run-pending, .run-running, .run-queued { color: var(--muted); }

/* --- comments ---------------------------------------------------------- */

.comments { padding: 8px 0 40px; }
.c { padding: 9px 0; border-top: 1px solid var(--rule); }
.c .meta { color: var(--muted); font-size: 12.5px; margin-bottom: 3px; }
.c .body { font-size: 14.5px; }
.c.dead { opacity: .55; }

/* --- forms ------------------------------------------------------------- */

form.stack { display: flex; flex-direction: column; gap: 10px; max-width: 100%; }
label { font-size: 13px; color: var(--ink-soft); font-weight: 600; }
input[type=text], input[type=url], textarea, select {
  width: 100%; font: inherit; color: var(--ink); background: var(--card);
  border: 1px solid var(--rule); border-radius: 4px; padding: 7px 9px;
}
textarea { font: 13.5px/1.6 var(--mono); min-height: 12em; resize: vertical; }
input:focus, textarea:focus, select:focus { outline: 2px solid var(--accent); outline-offset: -1px; }
.btn {
  font: 600 14px/1 inherit; padding: 9px 16px; border-radius: 4px; cursor: pointer;
  background: var(--accent); color: #fff; border: 1px solid var(--accent);
}
.btn:hover { filter: brightness(1.08); }
.btn-quiet { background: transparent; color: var(--accent); }
.hint { font-size: 12.5px; color: var(--muted); }

/* --- panels ------------------------------------------------------------ */

.panel {
  background: var(--card); border: 1px solid var(--rule);
  border-radius: 6px; padding: 14px 16px; margin: 14px 0;
}
.panel h2 { font: 600 15px/1.3 var(--serif); margin: 0 0 8px; }
.bar { height: 7px; background: var(--rule); border-radius: 4px; overflow: hidden; }
.bar > i { display: block; height: 100%; background: var(--accent); }
.grid { display: grid; gap: 12px; grid-template-columns: repeat(auto-fit, minmax(170px, 1fr)); }
.stat .k { font: 600 20px/1.2 var(--serif); }
.stat .l { font-size: 12.5px; color: var(--muted); }

.msg { padding: 9px 12px; border-radius: 4px; margin: 12px 0; font-size: 14px; }
.msg-error { background: var(--refuted-bg); color: var(--refuted); }
.msg-success { background: var(--proved-bg); color: var(--proved); }
.msg-info { background: var(--accent-dim); color: var(--ink-soft); }

footer.foot {
  border-top: 1px solid var(--rule); margin-top: 40px; padding: 18px 0 40px;
  font-size: 12.5px; color: var(--muted);
}
footer.foot a { color: var(--muted); }

/* KaTeX: long display formulas must scroll in their own box, never push the
   page sideways. */
.math-display { overflow-x: auto; overflow-y: hidden; padding: 2px 0; }
.katex { font-size: 1.05em; }

@media (max-width: 560px) {
  .item .n { display: none; }
  .masthead .wrap { gap: 10px; }
}