/* lf-lean: the Rocq/Lean card on marked words and the six-pair strip (static/js/lflean.js) */

body {
  --lfl-ink: var(--brand);                                       /* labels, the mark's underline */
  --lfl-wash: color-mix(in srgb, var(--brand) 14%, var(--paper)); /* hover / open background */
  --lfl-code: var(--ground);
  --lfl-rule: var(--line, color-mix(in srgb, var(--ink) 22%, var(--paper)));
  --lfl-dim: var(--dim, color-mix(in srgb, var(--ink) 62%, var(--paper)));
}

/* ---------- the mark ---------- */
.stmt {
  cursor: pointer; text-decoration: underline dotted; text-decoration-color: var(--lfl-ink);
  text-decoration-thickness: 2px; text-underline-offset: 4px;
}
.stmt:hover, .stmt[aria-expanded=true] { background: var(--lfl-wash); }
/* a tiny "two languages" glyph so the mark reads as a different thing from a link or a claim */
.stmt::after {
  content: '\21C4'; font-family: var(--font-mono); font-size: 0.7em; color: var(--lfl-ink);
  margin-left: 2px; vertical-align: 0.35em;
}

/* ---------- shared: a header line and a pair of code panes ---------- */
.lfl-head {
  display: flex; flex-wrap: wrap; gap: var(--sp-1) var(--sp-3); align-items: baseline;
  padding: 6px var(--sp-4); border-bottom: 1px solid var(--lfl-rule);
  font-family: var(--font-mono); font-size: 11px; color: var(--lfl-dim);
}
.lfl-head__name { font-size: 13px; font-weight: 600; color: var(--ink); }
.lfl-head__tag { text-transform: uppercase; letter-spacing: 0.08em; }
.lfl-head__tag--extreme { color: var(--ink); font-weight: 600; }
.lfl-pane__label {
  display: block; padding: 4px var(--sp-3); font-family: var(--font-mono); font-size: 11px; font-weight: 600;
  letter-spacing: 0.1em; text-transform: uppercase; color: var(--lfl-ink); border-bottom: 1px solid var(--lfl-rule);
}
.lfl-pane__label small { font-weight: 400; letter-spacing: 0.02em; text-transform: none; color: var(--lfl-dim); margin-left: var(--sp-2); }
/* code: unwrapped, so a line of Rocq stays a line; long Lean names scroll sideways inside the pane */
/* body … pre: outranks bench.css's .prose pre padding, which leaves room for a language tab */
body .prose pre.lfl-code, .lfl-code {
  margin: 0; padding: var(--sp-3) !important; border: 0 !important; background: var(--lfl-code) !important;
  font-family: var(--font-mono); font-size: 12px; line-height: 1.55; white-space: pre; overflow: auto;
  color: var(--ink);
}
.prose .lfl-code code { background: none !important; padding: 0 !important; font-size: inherit; }
.prose .lfl-code code::before { display: none; }
/* Lean names carry the Rocq module path (Original_LF__DOT__Imp_LF_Imp_…); dim it so the name reads */
.lfl-pfx { color: var(--lfl-dim); text-decoration: none; cursor: help; }
.lfl-foot {
  display: flex; flex-wrap: wrap; gap: var(--sp-1) var(--sp-4); justify-content: space-between;
  padding: 6px var(--sp-4); font-family: var(--font-mono); font-size: 11px; color: var(--lfl-dim);
  border-top: 1px solid var(--lfl-rule);
}
.lfl-foot a { color: var(--ink); }

/* ---------- the hover card ---------- */
.lfl-card {
  position: absolute; z-index: 60; width: calc(100vw - 32px);
  background: var(--paper); border: 1px solid var(--ink); box-shadow: 0 10px 30px rgba(0, 0, 0, 0.12);
  animation: lfl-in 140ms ease-out;
}
/* Lean lines run longer (every name carries its Rocq module path), so Lean gets the wider share */
.lfl-card__pair { display: grid; grid-template-columns: minmax(0, 2fr) minmax(0, 3fr); }
.lfl-card__pair > div + div { border-left: 1px solid var(--lfl-rule); }
.lfl-card .lfl-code { max-height: 300px; }
@keyframes lfl-in { from { opacity: 0; transform: translateY(-3px); } }

/* ---------- the translation strip ---------- */
.prose .lfl-strip[hidden] { display: none; }
.prose .post-figure.lfl-strip { padding-bottom: var(--sp-3); }
.lfl-strip__top { display: flex; flex-wrap: wrap; align-items: center; gap: var(--sp-2) var(--sp-4); margin-bottom: var(--sp-3); }
.lfl-strip__title { font-family: var(--font-mono); font-size: 13px; font-weight: 600; letter-spacing: 0.06em; text-transform: uppercase; color: var(--ink); margin-right: auto; }
.lfl-strip__nav { display: flex; align-items: center; gap: var(--sp-2); font-family: var(--font-mono); font-size: 12px; }
.lfl-strip__nav button {
  font: inherit; width: 32px; height: 32px; background: var(--paper); color: var(--ink);
  border: 1px solid var(--lfl-rule); cursor: pointer;
}
.lfl-strip__nav button:hover:not(:disabled) { border-color: var(--ink); }
.lfl-strip__nav button:disabled { opacity: 0.35; cursor: default; }
.lfl-strip__count { min-width: 3.5em; text-align: center; font-variant-numeric: tabular-nums; }
.lfl-strip__chapters { display: flex; flex-wrap: wrap; gap: var(--sp-1); margin: 0 0 var(--sp-3); padding: 0; list-style: none; }
.prose .lfl-strip__chapters li { margin: 0; }
/* the html prefix outranks bench.css's list-marker dash, which otherwise lands on the previous tab */
html .prose ul.lfl-strip__chapters { padding-left: 0; }
html .prose ul.lfl-strip__chapters li { list-style: none; }
html .prose ul.lfl-strip__chapters li::marker { content: none; }
.lfl-strip__chapters button {
  font-family: var(--font-mono); font-size: 11px; padding: 3px 8px; background: transparent; color: var(--lfl-dim);
  border: 1px solid var(--lfl-rule); cursor: pointer;
}
.lfl-strip__chapters button[aria-current=true] { background: var(--ink); color: var(--paper); border-color: var(--ink); }
.lfl-strip__track {
  display: flex; gap: var(--sp-4); overflow-x: auto; scroll-snap-type: x mandatory; scroll-behavior: smooth;
  overscroll-behavior-x: contain; scrollbar-width: thin;
}
.lfl-strip__track:focus-visible { outline: 2px solid var(--ink); outline-offset: 2px; }
.lfl-slide { flex: 0 0 100%; scroll-snap-align: start; background: var(--paper); border: 1px solid var(--lfl-rule); display: flex; flex-direction: column; min-width: 0; }
.lfl-slide__pair { display: grid; grid-template-columns: minmax(0, 2fr) minmax(0, 3fr); flex: 1; }
.lfl-slide__pair > div { min-width: 0; display: flex; flex-direction: column; }
.lfl-slide__pair > div + div { border-left: 1px solid var(--lfl-rule); }
.lfl-slide .lfl-code { flex: 1; max-height: 260px; }
.lfl-strip figcaption { margin-top: var(--sp-3) !important; }

@media (max-width: 640px) {
  /* phones: Rocq above Lean; the panes are too narrow to sit side by side */
  .lfl-card__pair, .lfl-slide__pair { grid-template-columns: 1fr; }
  .lfl-card__pair > div + div, .lfl-slide__pair > div + div { border-left: 0; border-top: 1px solid var(--lfl-rule); }
  .lfl-card .lfl-code { max-height: 200px; }
  .lfl-slide .lfl-code { max-height: 200px; }
  .lfl-strip__title { flex-basis: 100%; }
}
@media (prefers-reduced-motion: reduce) {
  .lfl-card { animation: none; }
  .lfl-strip__track { scroll-behavior: auto; }
}