/* Patavina presentation-specific refinements. */

@import url('https://fonts.googleapis.com/css2?family=Source+Sans+3:wght@300;400;500;600;700&display=swap');

:root {
  --presentation-font: 'Source Sans 3';
  --presentation-size: 3.4vh;
}

.slide-header {
  display: flex;
  align-items: center;
  gap: 0;
  margin-bottom: 0.5em;
}

.slide-header img {
  height: 6vh;
  flex-shrink: 0;
}

.slide-header::after {
  content: '';
  flex: 1;
  height: 1.5px;
  background: var(--lean-teal);
}

.title-slide .logo {
  height: 140px;
}

.title-slide .blue-band {
  background: #0073A3;
  flex: 1;
  padding: 1em 1.5em;
  display: flex;
  flex-direction: column;
  justify-content: flex-start;
}

.title-slide h1 {
  font-size: 2em;
  font-weight: 300;
  margin: 0 0 0.6em 0;
  color: #ffffff;
}

.title-slide .meta {
  font-size: 0.85em;
  font-weight: 300;
  color: #ffffff;
  line-height: 1.6;
}

.title-slide .meta strong {
  font-weight: 500;
  color: #ffffff;
}

.title-slide .date {
  font-size: 0.85em;
  font-weight: 300;
  color: rgba(255,255,255,0.8);
  margin-top: auto;
  padding-bottom: 0.5em;
}

.reveal ul ul {
  font-size: 1em;
}

.reveal ul li {
  margin-bottom: 0.25em;
}

.reveal ul.agenda {
  display: grid;
  gap: 5em;
  list-style: none;
  margin-top: 2em;
  padding: 0;
}

.reveal ul.agenda li {
  position: relative;
  min-height: 2.5em;
  margin: 0;
  padding: 0.55em 0.75em 0.55em 3.2em;
  border-left: 4px solid var(--lean-teal);
  background: #f8fafc;
}

.reveal ul.agenda li::before {
  position: absolute;
  left: 0.8em;
  top: 0.62em;
  color: var(--lean-teal);
  font-size: 0.85em;
  font-weight: 700;
}

.reveal ul.agenda strong {
  display: block;
  margin-bottom: 0.12em;
  font-size: 1.05em;
}

.reveal p.formalization-image {
  display: flex;
  justify-content: center;
  margin: 4vh 0 0.18em;
}

.reveal p.formalization-image img {
  width: min(92vw, 1320px);
  max-height: 64vh;
  object-fit: contain;
  border: 1px solid var(--border-code);
  background: #ffffff;
}

.reveal .slide-image-block {
  position: absolute;
  bottom: 12vh;
  left: 3vw;
  right: 3vw;
}

.reveal p.formalization-image-small {
  display: flex;
  justify-content: center;
  margin: 0 0 0.6em;
}

.reveal p.formalization-image-small img {
  width: min(80vw, 1050px);
  max-height: 46vh;
  object-fit: contain;
  border: 1px solid var(--border-code);
  background: #ffffff;
}

.reveal p.formalization-caption {
  color: var(--text-muted);
  font-size: 0.72em;
  font-style: italic;
  margin: 0;
  text-align: center;
}

.reveal pre {
  font-size: 0.68em;
  width: 100%;
  margin: 0.4em 0;
  box-shadow: none;
  border: 1px solid var(--border-code);
  border-radius: 6px;
  background: var(--bg-code);
}

.reveal pre code {
  padding: 0.8em 1em;
  max-height: 70vh;
  background: var(--bg-code);
}

.accent {
  color: var(--lean-teal);
  font-weight: 600;
}

.key-box {
  background: #ecfeff;
  border: 1px solid #a5f3fc;
  border-left: 4px solid var(--lean-teal);
  border-radius: 0 8px 8px 0;
  padding: 0.6em 1em;
  margin: 0.4em 0;
  font-size: 0.85em;
}

.key-box strong {
  color: var(--text-dark);
}

.reveal section[data-background-color="#0073A3"] {
  display: flex !important;
  flex-direction: column;
  justify-content: center;
}

.reveal section[data-background-color="#0073A3"] h1,
.reveal section[data-background-color="#0073A3"] h2 {
  color: #ffffff !important;
  font-size: 2em;
  font-weight: 300;
}

.reveal section[data-background-color="#0073A3"] p,
.reveal section[data-background-color="#0073A3"] li {
  color: rgba(255, 255, 255, 0.9);
  font-size: 1.1em;
}

.reveal section[data-background-color="#0073A3"] em {
  color: #a5f3fc;
}

.reveal section[data-background-color="#0073A3"] strong {
  color: #ffffff;
}

.reveal section[data-background-color="#0073A3"] code {
  background: rgba(255, 255, 255, 0.15);
  color: #ffffff;
}

.two-col {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 1.5em;
  align-items: start;
}

.reveal p.vspace,
.reveal p.vspace-sm,
.reveal p.vspace-lg { visibility: hidden; line-height: 0; font-size: 0; margin: 0 !important; }

.reveal p.vspace    { padding-top: 5vh !important; }

.reveal p.vspace-sm { padding-top: 2vh !important; }

.reveal p.vspace-lg { padding-top: 10vh !important; }

.reveal .lemma-box {
  border: 2px solid var(--lean-teal);
  background: #ecfeff;
  border-radius: 6px;
  padding: 0.5em 1.2em;
  margin: 0.6em auto;
  width: fit-content;
  max-width: 90%;
  text-align: center;
  font-size: 0.85em;
}

.reveal,
.reveal section {
  --verso-code-keyword-color: #cf222e;
  --verso-code-const-color: #0550ae;
  --verso-code-var-color: #1e293b;
  --verso-code-color: #1e293b;
  --verso-code-font-family: 'SF Mono', 'Menlo', 'Monaco', 'Consolas', monospace;
  --verso-info-indicator-color: var(--lean-teal);
  --verso-code-keyword-weight: 700;
}

.reveal code.hl.lean.block {
  background: var(--bg-code);
  border: 1px solid var(--border-code);
  border-radius: 6px;
  box-shadow: none;
  padding: 0.8em 1em;
  font-size: 0.5em;
  line-height: 1.55;
  width: 95%;
  max-width: 95%;
  text-align: left;
}

.code-with-panel {
  border: 1px solid var(--border-code);
  border-radius: 6px;
  overflow: hidden;
  box-shadow: none;
}

.code-with-panel > code.hl.lean.block {
  border: none;
  border-radius: 6px 0 0 6px;
  background: var(--bg-code);
}

.code-with-panel > .panel-cell {
  background: #f8fafc;
  border-left: 1px solid var(--border-code);
}

.code-with-panel > .info-panel,
.code-with-panel .info-panel {
  font-size: 0.45em;
  color: var(--text-dark);
}

.reveal section[data-state="compactness-slide"] .lean-word-logo {
  height: 1.15em;
  width: auto;
  vertical-align: -0.16em;
}

.reveal section[data-state="compactness-slide"] .code-with-panel {
  --code-ratio: 2.7fr;
  --panel-ratio: 1.05fr;
  width: 100%;
  max-width: 100%;
  margin: 0;
}

.reveal section[data-state="compactness-slide"] code.hl.lean.block {
  width: auto;
  max-width: 100%;
  max-height: 91vh;
  padding: 0.55em 0.75em;
  font-size: 0.48em;
  line-height: 1.18;
}

.reveal section[data-state="compactness-slide"] p.live-link-text {
  position: absolute;
  bottom: calc(2vh + 13vh / 2 + 10vh);
  left: 1.6vw;
  margin: 0;
  font-size: 1.4em;
  transform: translateY(50%);
}

.reveal section[data-state="compactness-slide"] p.live-link-qr {
  position: absolute;
  bottom: 5vh;
  right: 3vw;
  margin: 0;
}

.reveal section[data-state="compactness-slide"] p.live-link-qr img {
  height: 20vh;
  width: 20vh;
  max-width: none;
  max-height: none;
}

.reveal section[data-state="compactness-slide"] .info-panel {
  font-size: 0.34em;
  line-height: 1.25;
}

.reveal code.hl.lean.inline {
  background: #f1f5f9;
  border-radius: 3px;
  padding: 0.1em 0.3em;
  font-size: 0.85em;
}

.command-output.information {
  background: #ecfeff;
  border-color: var(--lean-teal);
  border-radius: 4px;
  font-size: 0.9em;
}

.reveal .hl.lean .has-info.information .token:not(.tactic-state):not(.tactic-state *),
.reveal .hl.lean .has-info.information .inter-text:not(.tactic-state):not(.tactic-state *) {
  text-decoration-color: rgba(8, 145, 178, 0.35);
}

.hl.lean .keyword {
  font-weight: 700 !important;
}

.hl.lean .var {
  font-style: normal !important;
}

.hl.lean .hover-container {
  display: block;
}

.reveal section img.img-tall {
  max-height: 70vh;
  max-width: 95%;
}

.reveal section img.img-small {
  max-height: 25vh;
  max-width: 40%;
}

.reveal section img.img-wide {
  max-width: 90%;
  max-height: 40vh;
}

.reveal .r-hstack {
  display: flex !important;
  flex-direction: row;
  align-items: flex-start;
  gap: 1.5em;
}

.reveal .r-hstack > ul {
  flex: 1;
}

.reveal .r-hstack > p {
  flex: 1;
}

.reveal .r-hstack > hr,
.reveal .r-hstack > p:empty {
  display: none;
}

.pipeline {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  justify-content: center;
  gap: 0.4em;
  margin: 0.8em 0;
  font-size: 0.6em;
}

.pipeline .step {
  background: #e0f2fe;
  border: 1.5px solid #0284c7;
  border-radius: 6px;
  padding: 0.4em 0.9em;
  color: #0c4a6e;
  font-weight: 500;
  white-space: nowrap;
}

.pipeline .step.highlight {
  background: #d1fae5;
  border-color: #059669;
  color: #064e3b;
}

.pipeline .arrow {
  color: #0891b2;
  font-size: 1.2em;
  font-weight: 600;
}

.reveal table {
  font-size: 0.75em;
  border-collapse: collapse;
  margin: 0.5em 0;
  width: 100%;
}

.reveal table th {
  background: var(--lean-teal);
  color: white;
  font-weight: 600;
  padding: 0.4em 0.8em;
  text-align: left;
}

.reveal table td {
  padding: 0.3em 0.8em;
  border-bottom: 1px solid var(--border-code);
}

.reveal table tr:nth-child(even) td {
  background: #f8fafc;
}

.reveal table.verso-table {
  width: auto;
  margin: 0.2em 0;
  font-size: 0.85em;
}

.reveal table.verso-table td,
.reveal table.verso-table th {
  font-variant-numeric: tabular-nums;
  padding: 0.2em 1em;
}

.reveal table.verso-table td code {
  background: transparent;
  padding: 0;
  font-size: 1em;
}

.reveal table.verso-table td p,
.reveal table.verso-table th p {
  margin: 0;
}

.reveal p.two-boxes {
  position: absolute;
  bottom: 14vh;
  left: 4%;
  border: 2px solid var(--lean-teal);
  background: #ecfeff;
  border-radius: 6px;
  padding: 0.6em 1.8em;
  text-align: center;
  font-size: 0.9em;
  width: 40%;
  margin: 0;
  min-height: 4em;
  display: flex;
  align-items: center;
  justify-content: center;
}

.reveal p.two-boxes + p.two-boxes {
  left: 52%;
}

.reveal p.thankyou-name {
  font-size: 1.4em;
  font-weight: 600;
  margin-top: 3em;
}

.reveal p.thankyou-links {
  font-size: 0.9em;
  color: var(--text-muted);
  margin-top: 0.5em;
}

.reveal p.thankyou-center {
  position: absolute;
  top: 50%;
  left: 50%;
  transform: translate(-50%, -50%);
  font-size: 2em;
  font-weight: 500;
  text-align: center;
  white-space: nowrap;
  margin: 0;
}