/* The three panes. The proof pane is a grid of rows, each row a gutter, a
   margin and a formula, so that a subproof indents and the margin connectives
   line up as they do in the document. */

/* Monokai chrome + token colors for proof formulas (matches /examples/ /interp/). */
:root {
  --ink: #f8f8f2;
  --dim: #75715e;
  --paper: #1e1f1c;
  --pane: #272822;
  --rule: #3e3d32;
  --focus: #49483e;
  --hot: #66d9ef;
  --hot-soft: #3e3d32;
  --bad: #f92672;
  --good: #a6e22e;
  --site: #e6db74;
  --site-soft: #3e3d32;
  --kw: #f92672;
  --op: #f92672;
  --num: #ae81ff;
  --str: #e6db74;
  --cmt: #75715e;
  --var: #a6e22e;
  --mono: ui-monospace, "DejaVu Sans Mono", "Fira Mono", Menlo, monospace;
  color-scheme: dark;
}

* { box-sizing: border-box; }

body {
  margin: 0;
  background: var(--paper);
  color: var(--ink);
  font: 15px/1.45 system-ui, -apple-system, "Segoe UI", sans-serif;
  height: 100vh;
}

/* The window is the three panes: the page itself never scrolls, each pane
   scrolls on its own, and what a pane says at its foot stays in view. */
#app { display: flex; flex-direction: column; height: 100%; }

header {
  display: flex;
  flex-direction: column;
  gap: 0;
  padding: 0;
  border-bottom: 1px solid var(--rule);
}

/* top nav matches deploy/aptop/site header.site — same links, full-bleed */
.site-bar {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0.75rem 1.5rem;
  padding: 0.55rem 1rem;
  border-bottom: 1px solid var(--rule);
  background: var(--pane);
}
.site-bar .brand {
  font-weight: 700;
  font-size: 1.05rem;
  color: var(--ink);
  text-decoration: none;
  letter-spacing: 0.02em;
}
.site-bar .brand span { color: var(--good); font-weight: 600; }
.site-bar .brand:hover { text-decoration: none; }
.site-nav {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0.85rem 1.25rem;
  flex: 1;
  justify-content: space-between;
  font-size: 0.95rem;
}
.site-nav .nav-local,
.site-nav .nav-hehner {
  display: flex;
  flex-wrap: wrap;
  gap: 0.85rem;
  align-items: baseline;
}
.site-nav .nav-hehner { margin-left: auto; }
.site-nav a { color: var(--hot); text-decoration: none; }
.site-nav a:hover { text-decoration: underline; }
.site-nav a[aria-current="page"] { color: var(--good); font-weight: 600; }
.site-nav a.ext { font-weight: 600; }
.site-nav a.ext.book { color: var(--hot); }
.site-nav a.ext.course { color: var(--good); }

.ampheck-bar {
  display: flex;
  align-items: baseline;
  flex-wrap: wrap;
  gap: 0.6rem 1rem;
  padding: 0.55rem 1rem;
}

h1 { font-size: 1.1rem; margin: 0; letter-spacing: 0.02em; }
.tagline { color: var(--dim); font-size: 0.85rem; }
/* Credit to the original Toronto Netty, under the title. */
.credit { margin: 0; padding: 0.15rem 1rem 0.4rem; color: var(--dim); font-size: 0.78rem; }
.credit a { color: inherit; text-decoration: underline; }

.toolbar { margin-left: auto; display: flex; gap: 0.4rem; flex-wrap: wrap; align-items: center; }

button, select, .load {
  font: inherit;
  font-size: 0.85rem;
  color: var(--ink);
  background: var(--pane);
  border: 1px solid var(--rule);
  border-radius: 5px;
  padding: 0.2rem 0.55rem;
  cursor: pointer;
}

button:hover:not(:disabled), select:hover, .load:hover { border-color: var(--hot); color: var(--hot); }
button:disabled { opacity: 0.45; cursor: default; }
.load input { display: none; }

.note-bar {
  padding: 0.35rem 1rem;
  font-size: 0.85rem;
  border-bottom: 1px solid var(--rule);
  background: var(--pane);
}
.note-bar.quiet { color: var(--dim); }
.note-bar.error { color: var(--bad); }

.panes {
  display: grid;
  grid-template-columns: minmax(0, 3fr) minmax(0, 1.2fr) minmax(0, 2fr);
  gap: 1px;
  background: var(--rule);
  flex: 1;
  min-height: 0;
}

@media (max-width: 950px) {
  .panes { grid-template-columns: 1fr; overflow-y: auto; }
  .pane { min-height: 60vh; }
}

.pane { background: var(--pane); display: flex; flex-direction: column; min-width: 0; }

.pane h2 {
  margin: 0;
  padding: 0.45rem 0.8rem;
  font-size: 0.75rem;
  font-weight: 600;
  text-transform: uppercase;
  letter-spacing: 0.08em;
  color: var(--dim);
  border-bottom: 1px solid var(--rule);
  display: flex;
  justify-content: space-between;
  gap: 1rem;
}
.pane h2 .sub { text-transform: none; letter-spacing: 0; font-weight: 400; }

.body { padding: 0.5rem 0.4rem; overflow: auto; flex: 1; min-height: 0; }
.quiet { color: var(--dim); font-size: 0.85rem; margin: 0.4rem 0.6rem; }
pre { margin: 0.2rem 0.6rem; font-family: var(--mono); font-size: 0.85rem; white-space: pre; }

/* a line of the proof */
.line, .entry {
  display: flex;
  align-items: baseline;
  gap: 0.35rem;
  padding: 0.05rem 0.3rem;
  font-family: var(--mono);
  font-size: 0.95rem;
  border-radius: 4px;
}
.line.focused { background: var(--focus); }

.gutter {
  min-width: 2.1rem;
  text-align: right;
  color: var(--dim);
  font-family: var(--mono);
  font-size: 0.8rem;
  background: none;
  border: none;
  padding: 0 0.2rem;
  cursor: default;
}
.gutter.movable { cursor: pointer; }
.gutter.movable:hover { color: var(--hot); text-decoration: underline; }

.caret { width: 0.6rem; color: var(--hot); }
.margin { min-width: 2.4rem; color: var(--dim); margin-left: calc(var(--depth, 0) * 1.6rem); }
.margin.direction { color: var(--ink); }

.formula { white-space: pre; }
.op { color: var(--op); }
/* Token classes from highlight.ts — same as site.css .cm-aptop-* */
.cm-aptop-keyword { color: var(--kw); font-weight: 600; }
.cm-aptop-operator { color: var(--op); }
.cm-aptop-number { color: var(--num); }
.cm-aptop-comment { color: var(--cmt); font-style: italic; }
.cm-aptop-bool { color: var(--num); }
.cm-aptop-string { color: var(--str); }
.cm-aptop-variable { color: var(--var); }
/* Hehner hint marks: \/ (∨) much bigger/bolder; /\ (∧) lighter — high contrast */
.cm-aptop-or {
  color: #f8f8f2;
  font-weight: 800;
  font-size: 1.35em;
  line-height: 1;
  vertical-align: -0.08em;
  text-shadow: 0 0 0.5px #f8f8f2;
}
.cm-aptop-and {
  color: #75715e;
  font-weight: 500;
  font-size: 1em;
}
.formula .atom { color: var(--ink); }


.operand { padding: 0 0.05rem; }
button.operand {
  font-family: var(--mono);
  font-size: inherit;
  border: 1px solid transparent;
  background: none;
  border-radius: 3px;
  padding: 0 0.15rem;
}
button.operand:hover { background: var(--hot-soft); border-color: var(--hot); color: var(--ink); }

/* the runs of two or more operands — the contiguous segments of an
   association — which have no place of their own in the line above */
.entry.segments { gap: 0.3rem; padding-top: 0; padding-bottom: 0.2rem; }
.runs-label { color: var(--dim); font-size: 0.8rem; }
button.operand.segment {
  border-color: var(--rule);
  border-style: dashed;
  color: var(--dim);
  font-size: 0.85rem;
}
button.operand.segment:hover {
  border-style: solid;
  border-color: var(--hot);
  background: var(--hot-soft);
  color: var(--ink);
}

/* the part of the line before the focus that the suggestion being pointed at
   would rewrite — the whole formula, one operand, or a run of them with the
   operators between; the run's own button under the line lights up with it */
.site {
  background: var(--site-soft);
  border-radius: 3px;
  box-shadow: 0 1px 0 var(--site);
  color: var(--ink);
}
button.operand.site, button.operand.segment.site {
  border-color: var(--site);
  border-style: solid;
  color: var(--ink);
}

.note { margin-left: auto; padding-left: 1.5rem; color: var(--dim); font-size: 0.8rem; font-family: var(--mono); }
.note.gap { color: var(--bad); font-weight: 700; }

.entry .expr { flex: 1; min-width: 8rem; font-family: var(--mono); }
.entry input {
  font: inherit;
  font-size: 0.9rem;
  color: var(--ink);
  background: var(--paper);
  border: 1px solid var(--rule);
  border-radius: 5px;
  padding: 0.15rem 0.4rem;
}
.entry input:focus { outline: none; border-color: var(--hot); }

.outcome {
  border-top: 1px solid var(--rule);
  padding: 0.5rem 0.9rem;
  font-family: var(--mono);
  font-size: 0.85rem;
  color: var(--dim);
}
.outcome.proved { color: var(--good); }

.law { font-family: var(--mono); font-size: 0.9rem; padding: 0.15rem 0.6rem; }

.suggestion {
  display: flex;
  align-items: baseline;
  gap: 0.35rem;
  width: 100%;
  text-align: left;
  border: 1px solid transparent;
  background: none;
  border-radius: 4px;
  padding: 0.1rem 0.3rem;
  font-family: var(--mono);
  font-size: 0.95rem;
}
.suggestion:hover:not(:disabled) { background: var(--hot-soft); border-color: var(--hot); }
.suggestion .margin { min-width: 1.4rem; }
.suggestion.blocked { opacity: 0.55; }
/* A conditional law whose premise is not settled: the step is offered, and it
   leaves the document's warning sign. The row is marked as the gapped lines of
   the proof pane are. */
.suggestion.gappy .note { color: var(--bad); }
/* The document's small dialog box: one field per law variable the match left
   unconstrained, opened by clicking the greyed row above it. */
.holes {
  display: flex; flex-wrap: wrap; gap: 0.4rem; align-items: center;
  padding: 0.35rem 0.6rem 0.5rem 2.1rem; border-bottom: 1px solid var(--rule);
  background: var(--hot-soft);
}
.holes label { display: inline-flex; gap: 0.3rem; align-items: center;
  font-family: var(--mono); font-size: 0.8rem; color: var(--dim); }
.holes input { font-family: var(--mono); font-size: 0.8rem; padding: 0.1rem 0.3rem;
  border: 1px solid var(--rule); border-radius: 3px; background: var(--pane); color: var(--ink); }
.holes button { font-size: 0.75rem; padding: 0.1rem 0.5rem; }

/* book/course links live in .site-nav .nav-hehner */

.book-calc {
  margin: 0;
  padding: 0.4rem 1rem 0.6rem;
  border-bottom: 1px solid var(--rule);
  background: var(--pane);
  max-height: 28vh;
  overflow: auto;
}
.book-calc summary {
  cursor: pointer;
  font-weight: 650;
  color: var(--hot);
  margin-bottom: 0.35rem;
}
.book-calc pre {
  margin: 0;
  font: 0.8rem/1.4 var(--mono);
  white-space: pre-wrap;
  color: var(--ink);
}

/* Hierarchical examples picker (chapter → section → proof) */
.examples-picker { position: relative; }
.examples-menu {
  position: relative;
  font-size: 0.85rem;
}
.examples-summary {
  list-style: none;
  cursor: pointer;
  color: var(--ink);
  background: var(--pane);
  border: 1px solid var(--rule);
  border-radius: 5px;
  padding: 0.2rem 0.55rem;
  user-select: none;
}
.examples-summary::-webkit-details-marker { display: none; }
.examples-menu[open] > .examples-summary {
  border-color: var(--hot);
  color: var(--hot);
}
.examples-panel {
  position: absolute;
  right: 0;
  top: calc(100% + 4px);
  z-index: 40;
  width: min(92vw, 28rem);
  max-height: min(70vh, 28rem);
  overflow: auto;
  background: var(--pane);
  border: 1px solid var(--rule);
  border-radius: 6px;
  box-shadow: 0 8px 24px rgba(0, 0, 0, 0.45);
  padding: 0.35rem 0.45rem 0.55rem;
}
.examples-panel .ex-group,
.examples-panel .ex-section {
  border: none;
  margin: 0.15rem 0;
}
.examples-panel .ex-group > summary,
.examples-panel .ex-section > summary {
  cursor: pointer;
  font-weight: 600;
  color: var(--hot);
  padding: 0.2rem 0.25rem;
}
.examples-panel .ex-section > summary {
  font-weight: 500;
  color: var(--ink);
  opacity: 0.9;
}
.examples-panel ul.ex-items,
.examples-panel ul.examples-flat {
  list-style: none;
  margin: 0.15rem 0 0.35rem;
  padding: 0 0 0 0.4rem;
}
.examples-panel li { margin: 0.12rem 0; }
.examples-panel button.ex-pass,
.examples-panel button.ex-fail,
.examples-panel button.ex-missing {
  display: block;
  width: 100%;
  text-align: left;
  font: inherit;
  font-size: 0.82rem;
  background: transparent;
  border: 1px solid transparent;
  border-radius: 4px;
  padding: 0.2rem 0.4rem;
  cursor: pointer;
}
.examples-panel button.ex-pass {
  color: var(--ink);
}
.examples-panel button.ex-pass:hover {
  border-color: var(--hot);
  color: var(--hot);
  background: rgba(255, 255, 255, 0.04);
}
/* FAIL: amber — broken calc, still openable */
.examples-panel button.ex-fail {
  color: #fc9867;
  font-size: 0.78rem;
}
.examples-panel button.ex-fail:hover {
  border-color: #fc9867;
  background: rgba(252, 152, 103, 0.08);
}
/* MISSING: dim/grey — stub or not-yet-proved, still openable */
.examples-panel button.ex-missing {
  color: var(--dim);
  font-size: 0.78rem;
  opacity: 0.9;
}
.examples-panel button.ex-missing:hover {
  border-color: var(--dim);
  color: var(--ink);
  opacity: 1;
  background: rgba(255, 255, 255, 0.04);
}

@media (max-width: 600px) {
  .examples-panel {
    position: fixed;
    left: 0.5rem;
    right: 0.5rem;
    width: auto;
    top: 3.5rem;
    max-height: 75vh;
  }
}

/* ---- The guided tutorial (src/tutorial.ts) ------------------------------
   A card between the note bar and the panes says what to do next; the thing
   to click pulses. On a phone the card sits at the foot of the screen so the
   panes can scroll beneath it. */
.toolbar button.tutorial-button { border-color: var(--site); color: var(--site); font-weight: 600; }

.tutorial {
  border-bottom: 1px solid var(--rule);
  background: #2f302a;
  padding: 0.5rem 1rem 0.6rem;
  font-size: 0.92rem;
  max-height: 40vh;
  overflow: auto;
  flex: none;
}
.tut-head { display: flex; flex-wrap: wrap; align-items: baseline; gap: 0.3rem 0.8rem; }
.tut-kicker { color: var(--site); font-size: 0.75rem; text-transform: uppercase; letter-spacing: 0.06em; }
.tut-title { font-size: 1rem; }
.tut-tools { margin-left: auto; display: flex; gap: 0.35rem; flex-wrap: wrap; }
.tutorial button.tut-small { font-size: 0.75rem; padding: 0.1rem 0.45rem; }
.tut-goal { margin: 0.35rem 0 0.2rem; display: flex; flex-wrap: wrap; align-items: baseline; gap: 0.2rem; }
.tut-label { color: var(--good); font-weight: 600; }
.tut-book { color: var(--dim); font-size: 0.82rem; }
.tut-inline, .tut-inline p { display: inline; margin: 0; }
.tut-say p, .tut-then p { margin: 0.3rem 0; max-width: 60rem; }
.tut-then { color: var(--dim); border-left: 2px solid var(--rule); padding-left: 0.6rem; }
code.tut-f { font-family: var(--mono); background: var(--paper); border: 1px solid var(--rule);
  border-radius: 3px; padding: 0 0.25rem; color: var(--ink); white-space: nowrap; }
.tut-dots { display: flex; gap: 0.3rem; margin: 0.25rem 0; }
.tut-dot { width: 0.55rem; height: 0.55rem; border-radius: 50%; background: var(--rule); }
.tut-dot.done { background: var(--good); }
.tut-dot.now { background: var(--site); }
.tut-actions { display: flex; gap: 0.5rem; align-items: center; margin-top: 0.4rem; flex-wrap: wrap; }
.tutorial button.tut-go { border-color: var(--site); color: var(--site); font-weight: 600; }
.tut-success { color: var(--good); font-weight: 600; margin: 0.3rem 0; }
.tut-warn { color: var(--bad); margin: 0.3rem 0; }
.tut-meta { color: var(--dim); font-size: 0.8rem; margin: 0.3rem 0; }
.tut-list { margin: 0.4rem 0; padding-left: 1.6rem; }
.tut-list li { margin: 0.15rem 0; }
.tutorial button.tut-lesson { font-size: 0.85rem; padding: 0.05rem 0.4rem; }
.tutorial button.tut-lesson.current { border-color: var(--site); }
.tutorial button.tut-lesson.done { color: var(--good); }
.tut-teaches { color: var(--dim); font-size: 0.8rem; }

@keyframes tut-pulse {
  0%, 100% { box-shadow: 0 0 0 0 rgba(230, 219, 116, 0.75); }
  50% { box-shadow: 0 0 0 5px rgba(230, 219, 116, 0); }
}
.tut-target, .tut-cta {
  outline: 2px solid var(--site);
  outline-offset: 1px;
  animation: tut-pulse 1.3s ease-in-out infinite;
  border-radius: 4px;
}
.pane.tut-target { outline-offset: -3px; animation: none; }
@media (prefers-reduced-motion: reduce) { .tut-target, .tut-cta { animation: none; } }

@media (max-width: 950px) {
  .tutorial {
    position: fixed; left: 0; right: 0; bottom: 0; z-index: 30;
    max-height: 42vh; border-top: 2px solid var(--site); border-bottom: none;
    box-shadow: 0 -6px 18px rgba(0, 0, 0, 0.5);
  }
  .panes.touring { padding-bottom: 44vh; }
}