:root {
  /* Both palettes are defined below, so the browser should not invert the
     page when the reader asks for dark. The blue and the gold are the
     logo's. */
  color-scheme: light dark;
  --bg: #f3f5f8;
  --card: #ffffff;
  --line: #dce2ea;
  --ink: #1b2430;
  --muted: #5d6877;
  --accent: #2774ae;
  --accent-fill: #dcebf7;
  --gold: #ffd100;
  --warn: #9a5b00;
  --bad: #b3261e;
  --bad-fill: #fbe9e7;
  --code: #f6f8fa;
  --sans: system-ui, -apple-system, "Segoe UI", Roboto, sans-serif;
  --mono: ui-monospace, SFMono-Regular, "SF Mono", Menlo, Consolas, monospace;
}

@media (prefers-color-scheme: dark) {
  :root {
    --bg: #14181d;
    --card: #1b2027;
    --line: #2d343d;
    --ink: #e4e8ec;
    --muted: #9aa3ad;
    --accent: #6cb0e8;
    --accent-fill: #1c3347;
    --gold: #f5c211;
    --warn: #e0a24a;
    --bad: #f28b82;
    --bad-fill: #3d1f1d;
    --code: #151a20;
  }
}

* { box-sizing: border-box; }

/* The `display: none` the browser gives the `hidden` attribute is a
   user-agent rule, which any rule here setting `display` overrides. Restated
   as an author rule so the attribute holds. */
[hidden] { display: none !important; }

body {
  margin: 0;
  background: var(--bg);
  color: var(--ink);
  font: 15px/1.55 var(--sans);
}

main {
  margin: 0 auto;
  padding: 1.5rem 2rem 4rem;
}

@media (max-width: 40rem) {
  main { padding: 1rem 1rem 3rem; }
}

header { margin-bottom: 1.5rem; max-width: 60rem; }

h1 { margin: 0 0 0.6rem; line-height: 0; }

/* The logo is the title: the compiler's name with decision and clause graphs. */
.logo { display: block; width: auto; height: 4.5rem; max-width: 100%; }

h2 {
  margin: 0;
  font-size: 1rem;
  font-weight: 600;
}

.lede { margin: 0; color: var(--muted); }

a { color: var(--accent); }

code {
  font: 0.9em/1 var(--mono);
  background: var(--code);
  border-radius: 3px;
  padding: 0.1em 0.3em;
}

.visually-hidden {
  position: absolute;
  width: 1px;
  height: 1px;
  overflow: hidden;
  clip-path: inset(50%);
  white-space: nowrap;
}

.card {
  background: var(--card);
  border: 1px solid var(--line);
  border-radius: 8px;
  padding: 1.1rem;
  margin-bottom: 1.25rem;
}

/* Input beside the controls once there is room for both. */
.io { display: grid; gap: 1.1rem; }

@media (min-width: 56rem) {
  .io { grid-template-columns: minmax(0, 1fr) 15rem; }
}

label {
  display: block;
  margin-bottom: 0.3rem;
  font-size: 12px;
  font-weight: 500;
  letter-spacing: 0.02em;
  text-transform: uppercase;
  color: var(--muted);
}

.examples {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 0.5rem 0.7rem;
  margin-bottom: 1rem;
}

.lead { font-size: 14px; font-weight: 500; }
#examples { display: flex; flex-wrap: wrap; gap: 0.4rem; }

#examples button {
  width: auto;
  padding: 0.3rem 0.75rem;
  border-color: transparent;
  border-radius: 999px;
  background: var(--accent-fill);
  color: var(--accent);
  font-size: 13px;
}

#examples button:hover:not(:disabled) {
  border-color: var(--accent);
  background: var(--card);
  color: var(--accent);
}

#examples button[aria-pressed="true"], #examples button[aria-pressed="true"]:hover:not(:disabled) {
  border-color: var(--accent);
  background: var(--accent);
  color: var(--card);
}

textarea, select, input {
  width: 100%;
  color: var(--ink);
  background: var(--card);
  border: 1px solid var(--line);
  border-radius: 5px;
  padding: 0.4rem 0.55rem;
  font: 14px/1.4 var(--sans);
}

/* The box grows to the height of the settings beside it. */
.cnf-input { display: flex; flex-direction: column; min-height: 20rem; }

textarea {
  flex: 1;
  min-height: 12rem;
  resize: vertical;
  font: 13px/1.45 var(--mono);
  background: var(--code);
}

textarea:disabled { color: var(--muted); }

textarea:focus, select:focus, input:focus, button:focus-visible, summary:focus-visible {
  outline: 2px solid var(--accent);
  outline-offset: 1px;
}

.input-head {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0.3rem 0.5rem;
  margin-bottom: 0.3rem;
}

.input-head label { margin-bottom: 0; }

/* A file held over the page will become the input. */
body.dropping textarea {
  outline: 2px dashed var(--accent);
  outline-offset: 1px;
}

.controls { display: grid; gap: 0.7rem; align-content: start; margin: 0; }
.field { margin: 0; }

button {
  width: 100%;
  padding: 0.5rem;
  border: 1px solid var(--accent);
  border-radius: 5px;
  background: var(--accent);
  color: var(--card);
  font: 500 15px/1.4 var(--sans);
  cursor: pointer;
}

button:hover:not(:disabled) { background: var(--card); color: var(--accent); }

/* Cancel takes Count's place while a run is on, and the pointer says the
   page is busy everywhere but on it. */
#cancel { background: var(--card); color: var(--accent); }
#cancel:hover { background: var(--accent); color: var(--card); }
body.busy, body.busy :not(#cancel) { cursor: progress; }
button:disabled { opacity: 0.45; cursor: default; }

#status, .note {
  margin: 0;
  font-size: 13px;
  color: var(--muted);
}

#status { overflow-wrap: anywhere; }

.result-head {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0.3rem 0.8rem;
  margin-bottom: 0.8rem;
}

.result-head button, #open, #clear {
  width: auto;
  padding: 0.1rem 0.55rem;
  font-size: 12px;
}

#stale { color: var(--warn); }

/* ------------------------------------------------------------- summary */

/* The answer, with the gold of the logo's nodes beside it. */
.answer {
  margin: 0 0 0.9rem;
  padding: 0.55rem 0.75rem;
  border-left: 4px solid var(--gold);
  background: var(--code);
  border-radius: 0 5px 5px 0;
  max-width: 60rem;
}

.answer .label {
  display: block;
  font-size: 12px;
  font-weight: 500;
  letter-spacing: 0.02em;
  text-transform: uppercase;
  color: var(--muted);
}

.answer b {
  font: 600 1.6rem/1.3 var(--mono);
  font-variant-numeric: tabular-nums;
  color: var(--accent);
  overflow-wrap: anywhere;
}

/* A weighted count's decimal value, beside the exact count. */
.answer .decimal {
  margin-left: 0.75rem;
  font: 400 1.1rem/1.3 var(--mono);
  color: var(--muted);
  white-space: nowrap;
}

.answer.unsatisfiable { border-left-color: var(--warn); }

.answer.failed {
  border-left-color: var(--bad);
  background: var(--bad-fill);
}

.answer.failed p { margin: 0; }

.answer strong { font-weight: 600; }

.answer pre {
  margin: 0.4rem 0 0;
  white-space: pre-wrap;
  overflow-wrap: anywhere;
  font: 13px/1.45 var(--mono);
}

.facts {
  display: grid;
  grid-template-columns: max-content minmax(0, 1fr);
  gap: 0.25rem 1rem;
  margin: 0 0 1rem;
  font-size: 14px;
}

.facts dt { color: var(--muted); }
.facts dd { margin: 0; overflow-wrap: anywhere; }

details { margin-top: 0.6rem; }

summary {
  cursor: pointer;
  font-size: 13px;
  color: var(--muted);
}

pre.block {
  max-height: 24rem;
  overflow: auto;
  margin: 0.4rem 0 0;
  padding: 0.6rem 0.75rem;
  border: 1px solid var(--line);
  border-radius: 6px;
  background: var(--code);
  font: 12.5px/1.5 var(--mono);
  white-space: pre-wrap;
  overflow-wrap: anywhere;
}

/* ------------------------------------------------------- the compile */

h3 {
  margin: 1.4rem 0 0.4rem;
  font-size: 0.95rem;
  font-weight: 600;
}

.explain { margin: 0 0 0.9rem; max-width: 60rem; font-size: 14px; }

.stepper {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 0.4rem;
}

.stepper button { width: auto; min-width: 2.4rem; padding: 0.2rem 0.6rem; font-size: 14px; }
#step-play { min-width: 5rem; }
.stepper input { flex: 1; min-width: 8rem; padding: 0; accent-color: var(--accent); }

.step-text { min-height: 3em; margin: 0.6rem 0; max-width: 60rem; font-size: 14px; }

/* The clauses beside the picture once there is room for both. */
.compile-grid { display: grid; gap: 1rem; align-items: start; }

@media (min-width: 56rem) {
  .compile-grid { grid-template-columns: 15rem minmax(0, 1fr); }
}

.clauses {
  max-height: 36rem;
  overflow: auto;
  margin: 0;
  padding: 0.4rem 0.6rem 0.4rem 2.4rem;
  border: 1px solid var(--line);
  border-radius: 6px;
  background: var(--code);
  font: 12.5px/1.7 var(--mono);
}

/* A clause waiting for its node, joining at the step on show, or in. */
.clauses li { color: var(--muted); border-radius: 3px; padding: 0 0.3rem; }
.clauses li.joining { color: var(--ink); background: color-mix(in srgb, var(--gold) 35%, transparent); }
.clauses li.in { color: var(--accent); }
.clauses li.lit { outline: 1px solid var(--accent); }

.picture {
  overflow: auto;
  max-height: 75vh;
  border: 1px solid var(--line);
  border-radius: 6px;
}

#picture { display: block; margin: 0 auto; font: 11px var(--mono); }
#picture text { text-anchor: middle; fill: var(--ink); }
/* The vtree is drawn as the tree the diagram grows on: broad, pale branches
   behind it. */
#picture .skeleton line { stroke: var(--line); stroke-width: 7; stroke-linecap: round; opacity: 0.6; }
#picture .skeleton circle { fill: var(--line); }
#picture .edges line, #picture .edges path { stroke: var(--muted); stroke-width: 1; fill: none; }
#picture .edges .dead { opacity: 0.2; }

#picture .node > circle { fill: var(--accent); }
#picture .node.top > circle { stroke: var(--gold); stroke-width: 3; }
#picture .node .value { text-anchor: start; fill: var(--muted); font-size: 10px; }
#picture .pair rect { fill: var(--card); stroke: var(--accent); }
#picture .pair text { font-size: 10.5px; }
#picture .pair line { stroke: var(--accent); }
#picture .pair circle { fill: var(--accent); }
#picture .dead { opacity: 0.3; }

#picture .constant circle { fill: var(--card); stroke-width: 2; }
#picture .constant text { font-size: 14px; }
#picture .constant.top circle { stroke: var(--muted); }
#picture .constant.bottom circle { stroke: var(--bad); }
#picture .constant.bottom text { fill: var(--bad); }

/* The clauses waiting at a node: outlined until the node's step, then gold. */
#picture .badge rect { fill: var(--card); stroke: var(--gold); stroke-width: 1.5; }
#picture .badge.placed rect { fill: var(--gold); }
#picture .badge text { font-size: 10px; fill: var(--ink); }
#picture .badge.placed text { fill: #1b2430; }
#picture .badge.lit rect { stroke: var(--accent); stroke-width: 2.5; }

#picture .leaf { cursor: pointer; }
#picture .leaf rect { fill: var(--code); stroke: var(--line); }
#picture .leaf.true rect { fill: var(--accent); stroke: var(--accent); }
#picture .leaf.true text { fill: var(--card); }
#picture .leaf.false rect { fill: var(--bad-fill); stroke: var(--bad); }
#picture .leaf.false text { fill: var(--bad); text-decoration: line-through; }
#picture .leaf.lit rect { stroke: var(--gold); stroke-width: 2.5; }

#picture .fresh { animation: appear 0.6s ease-out; }

@keyframes appear {
  from { opacity: 0; }
  to { opacity: 1; }
}

@media (prefers-reduced-motion: reduce) {
  #picture .fresh { animation: none; }
}

/* ------------------------------------------------------------ the ask */

.evidence {
  display: grid;
  grid-template-columns: max-content max-content minmax(6rem, 1fr) 4rem;
  align-items: center;
  gap: 0.3rem 0.8rem;
  max-width: 44rem;
}

/* Each row's four cells take the grid's columns. */
.ask-row { display: contents; }
.ask-row .variable { font: 13px var(--mono); }
.ask-row .share { font: 12.5px var(--mono); text-align: right; color: var(--muted); }

.pins { display: inline-flex; }
.pins button {
  width: auto;
  padding: 0.1rem 0.55rem;
  border-radius: 0;
  background: var(--card);
  color: var(--accent);
  font-size: 12px;
}
.pins button:first-child { border-radius: 5px 0 0 5px; }
.pins button:last-child { border-radius: 0 5px 5px 0; }
.pins button + button { border-left-width: 0; }
.pins button[aria-pressed="true"] { background: var(--accent); color: var(--card); }

.bar {
  height: 0.7rem;
  border-radius: 999px;
  background: var(--code);
  border: 1px solid var(--line);
  overflow: hidden;
}

.bar .fill { display: block; height: 100%; background: var(--gold); transition: width 0.3s; }

.ask-foot {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0.4rem 1rem;
  margin: 0.8rem 0;
}

.ask-foot p { margin: 0; font-size: 14px; }
#evidence-clear { width: auto; padding: 0.1rem 0.55rem; font-size: 12px; }