/* Single palette driven by CSS custom properties — one light set as
   root defaults, overridden in a `prefers-color-scheme: dark` media
   query. CM6 picks up its own `oneDark` theme via the script below,
   so the variables here only drive the surrounding chrome. */
:root {
  --bg: #fff;
  --fg: #111;
  --fg-muted: #666;
  --tab-fg: #333;
  --pre-bg: #f5f5f5;
  --border: #ddd;
  --border-soft: #e5e5e5;
  --ok-fg: #087a3c;
  --ok-bg: #ecfdf3;
  --ok-border: #abefc6;
  --bad-fg: #b42318;
  --bad-bg: #fdf2f2;
  --bad-border: #f5c2c0;
  --diag-bg: #fdf2f2;
  --diag-border: #b42318;
  --warn-bg: #fffaf0;
  --warn-border: #d4a017;
  --focus-ring: #4a9eff;
  --pill-bg: #f0f0f0;
  --pill-pending: #999;
  --pill-done-bg: #e3f7ec;
  --pill-done-fg: #087a3c;
}
@media (prefers-color-scheme: dark) {
  :root {
    --bg: #1a1a1a;
    --fg: #e0e0e0;
    --fg-muted: #999;
    --tab-fg: #c8c8c8;
    --pre-bg: #242424;
    --border: #333;
    --border-soft: #2a2a2a;
    --ok-fg: #3fb371;
    --ok-bg: #10291c;
    --ok-border: #2d5e3f;
    --bad-fg: #e07b75;
    --bad-bg: #2a1010;
    --bad-border: #5a2f2d;
    --diag-bg: #2a1010;
    --diag-border: #e07b75;
    --warn-bg: #2a2310;
    --warn-border: #d4a017;
    --focus-ring: #6fb2ff;
    --pill-bg: #2a2a2a;
    --pill-pending: #666;
    --pill-done-bg: #10291c;
    --pill-done-fg: #3fb371;
  }
}

html, body {
  background: var(--bg);
  color: var(--fg);
}
body {
  font: 14px/1.45 ui-monospace, Menlo, Consolas, monospace;
  max-width: 1200px;
  margin: 0 auto;
  padding: 1.5rem 1rem;
  display: flex;
  flex-direction: column;
  height: 100vh;
  overflow: hidden;
  box-sizing: border-box;
}

h1 {
  font-size: 1.25rem;
  margin: 0 0 1rem;
  display: flex;
  align-items: baseline;
  flex-wrap: wrap;
  gap: .4em;
}
h1 a {
  color: inherit;
  text-decoration: none;
}
h1 a:hover {
  text-decoration: underline;
}
h1 .muted {
  font-weight: normal;
  font-size: .75em;
}
h1 .header-link {
  margin-left: auto;
  font-size: .85em;
  font-weight: normal;
}

button {
  font: inherit;
  padding: .4em 1em;
  cursor: pointer;
  background: var(--bg);
  color: var(--fg);
  border: 1px solid var(--border);
  border-radius: 4px;
}
button:hover:not(:disabled) { border-color: var(--focus-ring); }
button:disabled { cursor: not-allowed; opacity: .6; }

select {
  font: inherit;
  padding: .2em .4em;
  background: var(--bg);
  color: var(--fg);
  border: 1px solid var(--border);
  border-radius: 4px;
}

.muted { color: var(--fg-muted); }

pre {
  background: var(--pre-bg);
  color: var(--fg);
  padding: .6em .8em;
  border-radius: 6px;
  overflow-x: auto;
  white-space: pre-wrap;
  margin: .2em 0;
  font-size: .85em;
}

/* Split-pane workbench: editor on the left, output on the right.
   Each pane is a flex column that owns its own scroll; `min-height: 0`
   on the grid children is what lets the inner `overflow: auto` track
   work instead of the pane ballooning to fit content. Collapses to a
   single column under ~900px. */
#workbench {
  display: grid;
  grid-template-columns: minmax(0, 1fr) 10px minmax(0, 1fr);
  flex: 1;
  min-height: 420px;
}

/* Splitter between the source pane and the output pane. The 14px middle
   column IS the entire visible gap between panes — the draggable zone
   matches the whitespace width 1:1 so the cursor-change aligns with
   what the eye reads as "the gap". Same shape as `#left-resizer`
   (transparent strip, turns blue on hover / drag). Drag logic in
   index.html rewrites `grid-template-columns` so the left column gets
   an explicit px width and the right stays `1fr`. Hidden in the
   mobile single-column layout below. */
#col-resizer {
  cursor: col-resize;
  background: transparent;
  border-radius: 3px;
  transition: background 120ms;
}
#col-resizer:hover, #col-resizer.dragging {
  background: var(--focus-ring);
}
.pane {
  display: flex;
  flex-direction: column;
  min-height: 0;
}
.pane-header {
  display: flex;
  align-items: center;
  gap: .5em;
  margin-bottom: .4em;
  flex-wrap: wrap;
}
#source-input {
  flex: 1;
  min-height: 0;
  display: flex;
}
#source-input .cm-editor {
  flex: 1;
  min-width: 0;
  min-height: 0;
  border: 1px solid var(--border);
  border-radius: 6px;
  font-size: 13px;
}
#source-input .cm-editor.cm-focused {
  outline: 2px solid var(--focus-ring);
  outline-offset: -2px;
}
#output-view {
  flex: 1;
  min-height: 0;
  display: flex;
}
#output-view .cm-editor {
  flex: 1;
  /* `min-width: 0` lets the editor shrink to its grid cell instead of
     inflating to its widest line (flex children default to
     `min-width: auto`). Without it, one multi-kilobyte SMT-LIB line
     pushes the whole right pane wider than the viewport; with it, CM6's
     own `.cm-scroller` takes over horizontal overflow. */
  min-width: 0;
  min-height: 0;
  border: 1px solid var(--border);
  border-radius: 0 6px 6px 6px;
  font-size: 13px;
}
/* Both CM6 instances live inside the workbench; CM6 sets its own default
   font on `.cm-scroller`, so override it back to the body's monospace
   stack in one place instead of per-instance. */
.cm-scroller {
  font-family: ui-monospace, Menlo, Consolas, monospace;
}
/* Source-editor decorations for diagnostics flagged by the loc
   extractor. Errors get a red wash, warnings a softer yellow — same
   severity palette as the diagnostic panes below the editor. */
/* Thin left-edge bars instead of full-line washes, so the syntax-
   highlighted text underneath reads at full contrast. Two layers:
   diagnostic bars (`cm-error-line` / `cm-warning-line`) anchored at
   the failing assert/expression line, and verdict bars
   (`cm-verdict-ok-line` / `cm-verdict-bad-line`) anchored at each
   verified function's definition line. Together they give an
   at-a-glance map: green bars next to functions that proved, red
   bars next to functions and asserts that didn't. */
.cm-error-line       { box-shadow: inset 3px 0 0 var(--bad-fg); }
.cm-warning-line     { box-shadow: inset 3px 0 0 var(--warn-fg, #b88500); }
.cm-verdict-ok-line  { box-shadow: inset 3px 0 0 var(--ok-fg); }
.cm-verdict-bad-line { box-shadow: inset 3px 0 0 var(--bad-fg); }
@media (max-width: 900px) {
  body {
    height: auto;
    overflow: visible;
  }
  #workbench {
    grid-template-columns: minmax(0, 1fr);
    flex: 0 0 auto;
    min-height: 0;
  }
  #col-resizer { display: none; }
  .pane { overflow: visible; }
  #source-input .cm-editor { min-height: 14em; }
  #output-view { min-height: 20em; }
}

.controls {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: .5em 1em;
  margin-top: .5em;
}
/* Push the trailing checkboxes (Auto, Use std) to the right edge of
   the controls row. `margin-left: auto` on a flex child collapses the
   gap before it, so this acts as a spacer regardless of how many
   items sit on its left. */
.controls-right {
  margin-left: auto;
  display: flex;
  align-items: center;
  gap: 1em;
}
/* Pin the idle width so a click-then-busy swap (label disappears,
   spinner appears) doesn't shrink the button mid-flight. Sized to
   fit "Run" with default button padding — the cold-load
   `Loading … libs…` text intentionally pushes past during pre-roll;
   the button is disabled then so the one-time width shift isn't
   perceived as jitter. */
#action-run {
  min-width: 4em;
}
/* Busy state: hide the label, show a small CSS ring centered in the
   button's place. `.busy` is toggled by `runVerify` / `runProgram`
   on entry / cleanup. Pure CSS animation — browser handles the
   frame loop. */
#action-run.busy #action-run-label { display: none; }
#action-run.busy::after {
  content: '';
  display: inline-block;
  width: .9em;
  height: .9em;
  vertical-align: -.15em;
  border: 2px solid currentColor;
  border-right-color: transparent;
  border-radius: 50%;
  animation: action-spin .8s linear infinite;
}
@keyframes action-spin { to { transform: rotate(360deg); } }
/* Prev/next buttons flanking the example dropdown: small chevron pills
   that sit inline with the dropdown at matching height. */
.source-nav {
  padding: .15em .5em;
  font-size: .85em;
  line-height: 1;
}
/* Reset button: only visible when the current example is dirty (see
   `source-reset`'s `hidden` attribute, toggled in index.html). Matches
   the dropdown's font-size so it doesn't tower over the row. */
.source-reset {
  padding: .2em .7em;
  font-size: .85em;
}
.hint {
  font-size: .8em;
}
/* Checkbox labels: the default baseline alignment leaves the box
   noticeably higher than the shrunken .hint text. Flexing the label
   with align-items: center lines the checkbox's midline up with the
   label text's midline. */
label.hint {
  display: inline-flex;
  align-items: center;
  gap: .35em;
}
label.hint > input[type="checkbox"] {
  margin: 0;
}

/* Tab strip selecting which IR stage shows in the output CM6 view
   below. Tabs are disabled until the matching section lands in
   `sectionCache`; the active tab sits flush with its CM6 body so the
   border reads as one continuous surface. */
.output-tabs {
  display: flex;
  flex-wrap: wrap;
  gap: .2em;
  border-bottom: 1px solid var(--border);
  margin-bottom: 0;
}
.tab {
  background: none;
  border: 1px solid transparent;
  border-bottom: none;
  /* Dedicated `--tab-fg` (not `--fg-muted`) because tab labels sit on
     the body background with no chrome around them — `--fg-muted`
     reads legibly on pills/borders but feels washed out here. Both
     palettes tune this one level closer to `--fg`. */
  color: var(--tab-fg);
  font: inherit;
  font-size: .8em;
  padding: .3em .7em;
  cursor: pointer;
  border-radius: 4px 4px 0 0;
}
.tab:hover:not(:disabled) { color: var(--fg); }
.tab.active {
  background: var(--pre-bg);
  color: var(--fg);
  border-color: var(--border);
  margin-bottom: -1px;
}
.tab:disabled { opacity: .4; cursor: not-allowed; }

/* Right-aligned actions group — Download (current IR tab) and Share
   link. Wrapped in `.tab-actions` with `margin-left: auto` so they pin
   to the far edge regardless of how many stage buttons are present or
   whether `.output-tabs` wraps. Using a wrapper (rather than a sibling
   selector on `.tab-action`) keeps the CSS unambiguous: no selector
   coincidence with `.tab` (which is also a `<button>`). */
.tab-actions {
  display: flex;
  gap: .2em;
  align-items: center;
  margin-left: auto;
}
.tab-action {
  background: none;
  border: 1px solid var(--border);
  color: var(--tab-fg);
  font: inherit;
  font-size: .8em;
  padding: .2em .7em;
  margin-bottom: .15em;
  cursor: pointer;
  border-radius: 4px;
}
.tab-action:hover:not(:disabled) { color: var(--fg); border-color: var(--focus-ring); }
.tab-action:disabled { opacity: .4; cursor: not-allowed; }

/* Subtab row: sits right under the top tab bar, above the CM6 view.
   Holds two kinds of children — variant pills (e.g. raw / SSA / flat
   inside AIR) and group-level controls (the VIR `Show vstd` toggle).
   The control block uses `margin-left: auto` so variants hug the left
   edge and controls hug the right. Pill styling keeps variants visually
   subordinate to the main tab strip above, and the wrapper hides itself
   when the row is empty so tabs with a single variant and no controls
   don't leave a dead band above the editor. */
.output-subtabs {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: .3em;
  padding: .3em 0;
}
.output-subtabs:empty { display: none; }
.subtab {
  background: none;
  border: 1px solid var(--border);
  color: var(--fg-muted);
  font: inherit;
  font-size: .75em;
  padding: .15em .6em;
  cursor: pointer;
  border-radius: 999px;
}
.subtab:hover:not(:disabled) { color: var(--fg); border-color: var(--focus-ring); }
.subtab.active {
  background: var(--pre-bg);
  color: var(--fg);
}
.subtab:disabled { opacity: .4; cursor: not-allowed; }

/* Group-level control in the subtab row (currently just VIR's
   `Show vstd`). `margin-left: auto` pushes it to the right edge, so the
   variant pills stay left-anchored and the toggle lands visually
   symmetric with the controls row on the left pane. */
.tab-control {
  display: inline-flex;
  align-items: center;
  gap: .35em;
  margin-left: auto;
  font-size: .75em;
}
.tab-control > input[type="checkbox"] { margin: 0; }

/* Verdict + diagnostics live under the source editor in the left
   pane. Capped height with internal scroll so a long rustc dump
   doesn't squeeze the editor; collapses to zero when no run has
   produced a verdict yet (so the source fills the whole pane). */
#meta-panel {
  flex: 0 1 auto;
  max-height: 30%;
  overflow-y: auto;
  min-height: 0;
}

/* Draggable splitter between the source editor and the diagnostics pane.
   `left-resizer` becomes visible only when there's diagnostic content to
   resize against — otherwise it renders as a dead band above an empty
   pane. Drag logic lives in index.html. */
#left-resizer {
  flex: 0 0 10px;
  cursor: row-resize;
  background: transparent;
  border-radius: 3px;
  transition: background 120ms;
}
#left-resizer:hover, #left-resizer.dragging {
  background: var(--focus-ring);
}
#left-pane:has(#meta-panel:empty) #left-resizer {
  display: none;
}

.verdict {
  padding: .5em .8em;
  border-radius: 6px;
  margin-bottom: .4em;
}
.verdict.ok {
  background: var(--ok-bg);
  border: 1px solid var(--ok-border);
}
.verdict.bad {
  background: var(--bad-bg);
  border: 1px solid var(--bad-border);
}
.verdict-status { font-size: 1rem; font-weight: bold; }
/* Run output: distinct from rustc diagnostics — monospace block per
   stream (stdout vs stderr), inside the verdict-style container so it
   sits in the same visual band as the verify verdict. Stderr is dimmed
   slightly so a stack of `[run]` status lines doesn't overpower the
   user's actual `print!` output. */
.run-output {
  font-family: var(--mono, monospace);
  font-size: .85em;
  margin: .3em 0 0;
  white-space: pre-wrap;
}
.run-output-stderr { color: var(--muted-fg, #888); }
/* Per-span colors keep the ✓ green and ✗ red inside the headline
   even when the row is bad-state (any failure → bad-bg container).
   Plain spans (e.g. the trailing error count) inherit the regular
   foreground. */
.verdict-status .ok  { color: var(--ok-fg); }
.verdict-status .bad { color: var(--bad-fg); }
/* Per-query rows. Listed under the headline status, one per Z3 check.
   Each row is a thin grid: status icon + function + kind + outcome.
   Failures get the bad-fg color on the icon + outcome; successes are
   muted so the eye lands on failures first. `.clickable` rows jump
   the source editor to the function's span on click. */
.verdict-list {
  margin-top: .3em;
  font-size: .82em;
  display: flex;
  flex-direction: column;
  gap: .15em;
}
.verdict-row {
  display: grid;
  grid-template-columns: 1.2em auto 1fr auto;
  gap: .4em;
  align-items: baseline;
  padding: .15em .3em;
  border-radius: 3px;
}
.verdict-row.clickable { cursor: pointer; }
.verdict-row.clickable:hover { background: var(--hover-bg, rgba(127,127,127,.12)); }
.verdict-icon {
  font-weight: bold;
  text-align: center;
  font-variant-numeric: tabular-nums;
}
.verdict-row.ok  .verdict-icon { color: var(--ok-fg); }
.verdict-row.bad .verdict-icon { color: var(--bad-fg); }
.verdict-fn { font-family: var(--mono-font, monospace); }
.verdict-kind { color: var(--fg-muted); }
.verdict-outcome {
  color: var(--bad-fg);
  font-style: italic;
  margin-left: auto;
}
.subtab-timing {
  margin-left: auto;
  font-size: .75em;
  color: var(--fg-muted);
  font-variant-numeric: tabular-nums;
}

/* One rustc/verus diagnostic per block, color-coded by severity. The
   `clickable` modifier marks messages whose `file:L:C` we managed to
   parse — those jump the source editor to the span on click and open
   the matching inline-lint tooltip. Hover highlights both the list
   item and the corresponding editor line so the two views stay
   visually linked. */
pre.diagnostic {
  background: var(--pre-bg);
  border-left: 3px solid var(--border);
  padding: .4em .6em;
  border-radius: 0 6px 6px 0;
  margin: .3em 0;
  font-size: .82em;
  white-space: pre-wrap;
  overflow-x: auto;
}
pre.diagnostic.error {
  background: var(--diag-bg);
  border-left-color: var(--diag-border);
}
pre.diagnostic.warning {
  background: var(--warn-bg);
  border-left-color: var(--warn-border);
}
pre.diagnostic.clickable { cursor: pointer; }
pre.diagnostic.clickable:hover { filter: brightness(0.97); }
@media (prefers-color-scheme: dark) {
  pre.diagnostic.clickable:hover { filter: brightness(1.3); }
}
/* Flash applied to the source-editor line that a clicked diagnostic
   points at, so the eye catches the jump target. */
.cm-diag-flash { background-color: var(--focus-ring) !important; }

/* Styled banner for `;; …` comment lines in the output view (applied by
   the `bannerLines` CM6 plugin in index.html). */
.cm-banner-line {
  border-left: 3px solid var(--focus-ring);
  font-weight: 600;
}

/* Clickable `input.rs:L:C` span links in the output view (applied by
   the `spanLinks` CM6 plugin). */
.cm-span-link {
  cursor: pointer;
  text-decoration: underline dotted;
  text-underline-offset: 2px;
}
.cm-span-link:hover {
  color: var(--focus-ring);
  text-decoration-style: solid;
}