/* ─── Fonts ────────────────────────────────────────────────────── */
@font-face {
  font-family: "et-book";
  src: url("https://gabriel-uzquiano.github.io/logic/libs/tufte-css-2015.12.29/et-book/roman-line-figures.ttf") format("truetype");
  font-weight: normal; font-style: normal;
}
@font-face {
  font-family: "et-book";
  src: url("https://gabriel-uzquiano.github.io/logic/libs/tufte-css-2015.12.29/et-book/display-italic-old-style-figures.ttf") format("truetype");
  font-weight: normal; font-style: italic;
}
@font-face {
  font-family: "et-book";
  src: url("https://gabriel-uzquiano.github.io/logic/libs/tufte-css-2015.12.29/et-book/bold-line-figures.ttf") format("truetype");
  font-weight: bold; font-style: normal;
}

/* ─── Design tokens — course palette (identical to model checker) */
:root, [data-theme="light"] {
  --text-xs:   clamp(0.875rem, 0.82rem + 0.25vw, 1rem);
  --text-sm:   clamp(1rem,     0.95rem + 0.35vw, 1.125rem);
  --text-base: clamp(1.125rem, 1.05rem + 0.35vw, 1.25rem);
  --text-lg:   clamp(1.25rem,  1.1rem  + 0.75vw, 1.625rem);
  --text-xl:   clamp(1.625rem, 1.3rem  + 1.25vw, 2.375rem);

  --space-1: 0.25rem; --space-2: 0.5rem;  --space-3: 0.75rem;
  --space-4: 1rem;    --space-5: 1.25rem; --space-6: 1.5rem;
  --space-8: 2rem;

  --color-bg:             #ffffff;
  --color-surface:        #fafaf8;
  --color-surface-2:      #ffffff;
  --color-surface-offset: #f5f3ef;
  --color-border:         #ddd8ce;
  --color-divider:        #e8e4dd;

  --color-text:         #111111;
  --color-text-muted:   #555550;
  --color-text-faint:   #aaa8a2;

  --color-primary:           #7a1a3a;
  --color-primary-hover:     #5e1229;
  --color-primary-active:    #420c1c;
  --color-primary-highlight: #f5e8ec;

  --color-teal:           #006666;
  --color-teal-hover:     #004d4d;
  --color-teal-highlight: #e0f2f1;

  /* Truth / False — same as model checker */
  --color-true:        #2e7d32;
  --color-true-bg:     #f1f8e9;
  --color-true-border: #a5d6a7;
  --color-false:       #b71c1c;
  --color-false-bg:    #fce8e8;
  --color-false-border:#ef9a9a;

  --color-header-bg:   #2c2c2c;
  --color-header-text: #ffffff;

  /* Truth table main-connective column */
  --color-main-col-bg:     #fff8e1;
  --color-main-col-border: #f9a825;

  /* Highlighted consistency row */
  --color-row-hl-bg:     #e8f5e9;
  --color-row-hl-border: #a5d6a7;

  --radius-sm:   0.25rem; --radius-md: 0.375rem;
  --radius-lg:   0.5rem;  --radius-full: 9999px;
  --transition:  160ms cubic-bezier(0.16, 1, 0.3, 1);
  --shadow-sm:   0 1px 3px rgba(0,0,0,0.06);
  --shadow-md:   0 4px 12px rgba(0,0,0,0.08);

  --font-body: 'et-book', 'Palatino Linotype', 'Book Antiqua', Palatino, Georgia, serif;
  --font-mono: 'Consolas', 'Liberation Mono', Menlo, Courier, monospace;
  --font-sans: 'Gill Sans', 'Gill Sans MT', Calibri, sans-serif;
}

[data-theme="dark"] {
  --color-bg:              #16140f;
  --color-surface:         #1c1a14;
  --color-surface-2:       #211f19;
  --color-surface-offset:  #27251e;
  --color-border:          #3a3830;
  --color-divider:         #2e2c25;
  --color-text:            #d8d4cc;
  --color-text-muted:      #7e7a72;
  --color-text-faint:      #525049;
  --color-primary:         #e8779a;
  --color-primary-hover:   #d45a80;
  --color-primary-active:  #bd3d66;
  --color-primary-highlight: #3a1e26;
  --color-teal:            #4db6ac;
  --color-teal-hover:      #26a69a;
  --color-teal-highlight:  #1a302e;
  --color-true:            #66bb6a;
  --color-true-bg:         #1a2e1b;
  --color-true-border:     #2e5430;
  --color-false:           #ef5350;
  --color-false-bg:        #2d1414;
  --color-false-border:    #5c2828;
  --color-main-col-bg:     #2a2208;
  --color-main-col-border: #c8960a;
  --color-row-hl-bg:       #1a2e1b;
  --color-row-hl-border:   #2e5430;
  --shadow-sm: 0 1px 3px rgba(0,0,0,0.3);
  --shadow-md: 0 4px 12px rgba(0,0,0,0.4);
}

/* ─── Base reset ──────────────────────────────────────────────── */
*, *::before, *::after { box-sizing: border-box; margin: 0; padding: 0; }
[hidden] { display: none !important; }
html { -webkit-font-smoothing: antialiased; scroll-behavior: smooth; }
body {
  font-family: var(--font-body);
  font-size: var(--text-base);
  color: var(--color-text);
  background: var(--color-bg);
  min-height: 100dvh;
  line-height: 1.65;
}
code, .mono { font-family: var(--font-mono); }
button { cursor: pointer; background: none; border: none; font: inherit; color: inherit; }
input { font: inherit; color: inherit; }
::selection { background: var(--color-primary-highlight); color: var(--color-text); }
:focus-visible { outline: 2px solid var(--color-primary); outline-offset: 2px; border-radius: var(--radius-sm); }

/* ─── Header ──────────────────────────────────────────────────── */
.app-header {
  background: var(--color-bg);
  border-bottom: 1px solid var(--color-border);
  position: sticky; top: 0; z-index: 100;
}
.header-inner {
  max-width: 900px;
  margin: 0 auto;
  padding: var(--space-3) var(--space-6);
  display: flex; align-items: baseline; justify-content: space-between;
}
.logo, .header-brand { display: flex; align-items: baseline; gap: 2.5rem; }
.logo-text {
  font-size: var(--text-lg); font-weight: normal; font-style: italic;
  color: var(--color-text); font-family: var(--font-body);
}
.logo-subtitle {
  font-size: var(--text-sm); color: var(--color-text-muted); font-family: var(--font-sans);
}
.header-right { display: flex; align-items: center; gap: var(--space-5); }
.help-link {
  font-size: var(--text-sm); font-family: var(--font-sans);
  color: var(--color-text-muted); text-decoration: none;
  transition: color var(--transition);
}
.help-link:hover { color: var(--color-primary); }
.theme-toggle {
  width: 32px; height: 32px;
  display: flex; align-items: center; justify-content: center;
  border-radius: var(--radius-full);
  color: var(--color-text-muted);
  transition: background var(--transition), color var(--transition);
}
.theme-toggle:hover { background: var(--color-surface-offset); color: var(--color-text); }

/* ─── Help Panel ──────────────────────────────────────────────── */
.help-panel {
  background: var(--color-surface);
  border-bottom: 1px solid var(--color-border);
  padding: var(--space-6);
}
.help-inner { max-width: 900px; margin: 0 auto; }
.help-panel h2 {
  font-size: var(--text-lg); font-weight: normal; font-style: italic;
  margin-bottom: var(--space-4); color: var(--color-primary);
}
.help-panel h3 {
  font-size: var(--text-sm); font-weight: 600; font-family: var(--font-sans);
  text-transform: uppercase; letter-spacing: 0.06em;
  color: var(--color-text-muted); margin-bottom: var(--space-2);
}
.help-grid { display: grid; grid-template-columns: 1fr 1fr; gap: var(--space-8); }
@media (max-width: 640px) { .help-grid { grid-template-columns: 1fr; } }
.help-table { width: 100%; border-collapse: collapse; font-size: var(--text-sm); }
.help-table th {
  text-align: left; padding: var(--space-2) var(--space-3);
  border-bottom: 2px solid var(--color-border);
  color: var(--color-text-muted); font-weight: 600; font-family: var(--font-sans);
  font-size: var(--text-xs); text-transform: uppercase; letter-spacing: 0.04em;
}
.help-table td { padding: var(--space-2) var(--space-3); border-bottom: 1px solid var(--color-divider); }
.help-list {
  list-style: none; display: flex; flex-direction: column;
  gap: var(--space-3); font-size: var(--text-sm); padding: 0;
}
.help-list li { line-height: 1.5; }
.close-help { margin-top: var(--space-5); }

/* ─── Main layout — single column, max-width ─────────────────── */
.app-main {
  max-width: 900px;
  margin: 0 auto;
  padding: var(--space-6);
  display: flex;
  flex-direction: column;
  gap: var(--space-5);
}

/* ─── Cards ───────────────────────────────────────────────────── */
.card {
  background: var(--color-surface);
  border: 1px solid var(--color-border);
  border-radius: var(--radius-md);
  padding: var(--space-5);
  box-shadow: var(--shadow-sm);
  display: flex; flex-direction: column; gap: var(--space-4);
}
.card-header {
  display: flex; align-items: center; justify-content: space-between;
  gap: var(--space-3); flex-wrap: wrap;
  border-bottom: 1px solid var(--color-divider);
  padding-bottom: var(--space-3);
}
.section-title {
  font-size: var(--text-base); font-weight: normal; font-style: italic;
  color: var(--color-primary);
}
.card-hint {
  font-size: var(--text-sm); color: var(--color-text-muted);
  font-family: var(--font-body); font-style: italic;
}

/* ─── Symbol toolbar ──────────────────────────────────────────── */
.input-toolbar { display: flex; gap: var(--space-1); flex-wrap: wrap; }
.sym-btn {
  font-family: var(--font-body); font-size: var(--text-base); line-height: 1;
  padding: 3px var(--space-2);
  border: 1px solid var(--color-border); border-radius: var(--radius-sm);
  background: var(--color-surface-2); color: var(--color-primary);
  transition: background var(--transition), border-color var(--transition);
}
.sym-btn:hover { background: var(--color-primary-highlight); border-color: var(--color-primary); }

/* ─── Formula input / slots ───────────────────────────────────── */
.formula-input-wrap { position: relative; }
.formula-input {
  width: 100%;
  padding: var(--space-3) var(--space-4);
  font-family: var(--font-mono); font-size: var(--text-base);
  background: var(--color-surface-2);
  border: 1px solid var(--color-border); border-radius: var(--radius-md);
  transition: border-color var(--transition), box-shadow var(--transition);
}
.formula-input:focus {
  outline: none; border-color: var(--color-primary);
  box-shadow: 0 0 0 3px var(--color-primary-highlight);
}
.formula-input.valid   { border-color: var(--color-teal); }
.formula-input.invalid { border-color: var(--color-false); }

.parse-tick {
  position: absolute; right: 10px; top: 50%; transform: translateY(-50%);
  color: var(--color-teal); font-size: var(--text-base); pointer-events: none;
}
.parse-status {
  font-size: var(--text-sm); color: var(--color-text-muted);
  min-height: 1.4em; font-family: var(--font-body); font-style: italic;
}
.parse-status.ok  { color: var(--color-teal); }
.parse-status.err { color: var(--color-false); font-style: normal; font-family: var(--font-mono); font-size: var(--text-xs); }

/* Multi-formula slots */
.formula-slot {
  display: grid; grid-template-columns: auto 1fr auto;
  align-items: start; gap: var(--space-3);
  padding: var(--space-3) 0;
  border-bottom: 1px solid var(--color-divider);
}
.formula-slot:last-child { border-bottom: none; }
.slot-label {
  font-family: var(--font-body); font-style: italic;
  font-size: var(--text-base); color: var(--color-text-muted);
  padding-top: 10px; min-width: 2rem;
}
.slot-remove { margin-top: 8px; color: var(--color-text-faint); padding: 4px; border-radius: var(--radius-sm); }
.slot-remove:hover { color: var(--color-false); background: var(--color-false-bg); }
.formula-add-row { padding: var(--space-2) 0 0; display: flex; }

/* ─── Example chips ───────────────────────────────────────────── */
.formula-examples { display: flex; align-items: center; gap: var(--space-2); flex-wrap: wrap; }
.examples-label { font-size: var(--text-xs); color: var(--color-text-muted); font-family: var(--font-sans); flex-shrink: 0; }
.example-chip {
  font-family: var(--font-mono); font-size: var(--text-xs);
  padding: 2px var(--space-3);
  border: 1px solid var(--color-border); border-radius: var(--radius-full);
  background: transparent; color: var(--color-text-muted);
  transition: all var(--transition);
}
.example-chip:hover { border-color: var(--color-teal); color: var(--color-teal); background: var(--color-teal-highlight); }
.example-chip.active { border-color: var(--color-teal); color: var(--color-teal); background: var(--color-teal-highlight); }

/* ─── Buttons ─────────────────────────────────────────────────── */
.btn {
  display: inline-flex; align-items: center; justify-content: center; gap: var(--space-2);
  padding: var(--space-2) var(--space-5);
  border-radius: var(--radius-sm);
  font-size: var(--text-sm); font-family: var(--font-sans); font-weight: 600;
  letter-spacing: 0.02em; transition: all var(--transition); white-space: nowrap;
}
.btn-primary { background: var(--color-primary); color: #fff; border: 1px solid var(--color-primary); }
.btn-primary:hover { background: var(--color-primary-hover); border-color: var(--color-primary-hover); }
.btn-ghost { background: transparent; color: var(--color-text-muted); border: 1px solid var(--color-border); }
.btn-ghost:hover { border-color: var(--color-text-muted); color: var(--color-text); background: var(--color-surface-offset); }
.btn-sm { padding: 2px var(--space-3); font-size: var(--text-xs); }
.eval-row { display: flex; justify-content: flex-end; gap: var(--space-3); margin-top: var(--space-2); }

/* ─── Truth Table ─────────────────────────────────────────────── */
.tt-scroll { overflow-x: auto; }
.tt-wrap { margin-top: var(--space-2); }
.tt-formula-label {
  font-family: var(--font-body); font-style: italic;
  font-size: var(--text-base); color: var(--color-primary);
  margin-bottom: var(--space-2);
}
.truth-table {
  border-collapse: collapse;
  font-family: var(--font-body);
  font-size: var(--text-base);
  width: 100%;
}

/* Header row */
.truth-table thead th {
  font-family: var(--font-sans);
  font-style: normal;
  font-weight: normal;
  font-size: var(--text-sm);
  color: var(--color-text-muted);
  padding: var(--space-2) var(--space-3);
  text-align: center;
  border-bottom: 2px solid var(--color-border);
  white-space: nowrap;
}
.truth-table thead th.col-sep { border-right: 2px solid var(--color-border); }
.truth-table thead th.col-main {
  background: var(--color-main-col-bg);
  border-left: 2px solid var(--color-main-col-border);
  border-right: 2px solid var(--color-main-col-border);
  color: var(--color-text);
}

/* Body cells */
.truth-table tbody td {
  text-align: center;
  padding: var(--space-2) var(--space-3);
  border-bottom: 1px solid var(--color-divider);
  font-family: var(--font-sans);
  font-style: normal;
  font-size: var(--text-base);
}
.truth-table tbody td.col-sep { border-right: 2px solid var(--color-border); }
.truth-table tbody td.col-main {
  background: var(--color-main-col-bg);
  border-left: 2px solid var(--color-main-col-border);
  border-right: 2px solid var(--color-main-col-border);
}

/* T / F values — upright sans-serif */
.tv-T {
  color: var(--color-teal);
  font-family: var(--font-sans);
  font-style: normal;
  font-weight: normal;
}
.tv-F {
  color: var(--color-primary);
  font-family: var(--font-sans);
  font-style: normal;
  font-weight: normal;
}

/* Highlighted consistent row */
.truth-table tbody tr.row-consistent td {
  background: var(--color-row-hl-bg);
}
.truth-table tbody tr.row-consistent td.col-main {
  background: color-mix(in srgb, var(--color-row-hl-bg) 80%, var(--color-main-col-bg) 20%);
  border-left-color: var(--color-row-hl-border);
  border-right-color: var(--color-row-hl-border);
}

/* Counterexample row (validity / future use) */
.truth-table tbody tr.row-counterex td {
  background: var(--color-false-bg);
}
.truth-table tbody tr.row-counterex td.col-main {
  background: color-mix(in srgb, var(--color-false-bg) 80%, var(--color-main-col-bg) 20%);
}

/* ─── Build-mode cell buttons ─────────────────────────────────── */
.cell-btn {
  min-width: 2.2rem; min-height: 1.8rem;
  padding: 2px var(--space-2);
  border: 1px solid var(--color-border); border-radius: var(--radius-sm);
  background: var(--color-surface-2);
  font-family: var(--font-sans); font-style: normal; font-size: var(--text-base);
  color: var(--color-text-faint);
  transition: all var(--transition);
  cursor: pointer;
}
.cell-btn:hover { border-color: var(--color-teal); background: var(--color-teal-highlight); }
.cell-btn.filled { color: var(--color-text); border-color: var(--color-border); }
.cell-btn[data-val="T"] { color: var(--color-teal); font-weight: normal; }
.cell-btn[data-val="F"] { color: var(--color-primary); font-weight: normal; }

/* After check: correct / wrong feedback */
.cell-btn.correct {
  background: var(--color-true-bg);
  border-color: var(--color-true-border);
  pointer-events: none;
}
.cell-btn.correct[data-val="T"] { color: var(--color-true); }
.cell-btn.correct[data-val="F"] { color: var(--color-true); }
.cell-btn.wrong {
  background: var(--color-false-bg);
  border-color: var(--color-false-border);
  pointer-events: none;
}
.cell-btn.wrong[data-val="T"],
.cell-btn.wrong[data-val="F"] { color: var(--color-false); }

/* ─── Verdict banners ─────────────────────────────────────────── */
.verdict {
  padding: var(--space-3) var(--space-4);
  border-radius: var(--radius-sm);
  font-family: var(--font-body); font-style: italic; font-size: var(--text-base);
  display: flex; align-items: flex-start; gap: var(--space-3);
}
.verdict-icon { flex-shrink: 0; font-style: normal; }
.verdict.verdict-ok {
  background: var(--color-true-bg); color: var(--color-true);
  border: 1px solid var(--color-true-border);
}
.verdict.verdict-fail {
  background: var(--color-false-bg); color: var(--color-false);
  border: 1px solid var(--color-false-border);
}
.verdict.verdict-warn {
  background: var(--color-primary-highlight); color: var(--color-primary);
  border: 1px solid var(--color-border); border-left: 3px solid var(--color-primary);
}
.verdict strong { font-style: normal; font-weight: bold; font-family: var(--font-sans); font-size: var(--text-sm); letter-spacing: 0.03em; }

/* ─── Per-formula column blocks in Check view ─────────────────── */
.tt-formula-header {
  font-family: var(--font-body); font-style: italic; font-size: var(--text-sm);
  color: var(--color-text-muted); margin-top: var(--space-4);
  padding-bottom: var(--space-1); border-bottom: 1px solid var(--color-divider);
  margin-bottom: var(--space-1);
}

/* Separator between letter block and formula blocks */
.truth-table thead th.col-block-sep,
.truth-table tbody td.col-block-sep {
  border-right: 2px solid var(--color-border);
}

/* ─── Scrollbar ───────────────────────────────────────────────── */
.tt-scroll::-webkit-scrollbar { height: 4px; }
.tt-scroll::-webkit-scrollbar-track { background: transparent; }
.tt-scroll::-webkit-scrollbar-thumb { background: var(--color-border); border-radius: 2px; }