/* ========== Blueprint Page Styles ========== */
/* Note: This file depends on common.css being loaded first.
   common.css provides: sbs layout, proof toggles, Lean syntax, Tippy themes, modals, CSS variables */

/* ========== Theme Blue Base (from plasTeX) ========== */
@charset "UTF-8";
a,abbr,acronym,address,applet,article,aside,audio,b,big,blockquote,body,canvas,caption,center,cite,code,dd,del,details,dfn,div,dl,dt,em,embed,fieldset,figcaption,figure,footer,form,h1,h2,h3,h4,h5,h6,header,hgroup,html,i,iframe,img,ins,kbd,label,legend,li,mark,menu,nav,object,ol,output,p,pre,q,ruby,s,samp,section,small,span,strike,strong,sub,summary,sup,table,tbody,td,tfoot,th,thead,time,tr,tt,u,ul,var,video{font:inherit;font-size:100%;margin:0;padding:0;border:0}
article,aside,details,figcaption,figure,footer,header,hgroup,menu,nav,section{display:block}
body{line-height:1;overflow-x:hidden;background:var(--sbs-bg-page)}
ol,ul{list-style:none}
blockquote,q{quotes:none}
blockquote:after,blockquote:before,q:after,q:before{content:"";content:none}
table{border-spacing:0;border-collapse:collapse}
.clear:after{font-size:0;display:block;visibility:hidden;clear:both;height:0;content:" "}
.clear{display:inline-block}
* html .clear{height:1%}
.clear{display:block}
*{box-sizing:border-box}
hr{clear:both;border:none;outline:none}
em{font-style:italic}
a{text-decoration:underline;color:var(--sbs-link)}
a:hover{color:var(--sbs-link-hover)}
ul{list-style:disc}
ol{list-style:decimal}
ol,ul{font-size:14px;padding:0 0 0 33px}
ol li,ul li{margin:0}
blockquote{padding:0 15px 0 40px}
table{font-size:13px;width:100%;margin:20px 0;background:var(--sbs-bg-surface)}
table th{font-size:16px;font-weight:700}
table tr td{padding:7px}
::selection{color:var(--sbs-selection-text);background:var(--sbs-selection-bg)}
::-moz-selection{color:var(--sbs-selection-text);background:var(--sbs-selection-bg)}
body{height:100vh;margin:0;flex-direction:column;color:var(--sbs-text);background-color:var(--sbs-bg-page)}
body,div.wrapper{display:flex;overflow:hidden}
div.wrapper{flex-grow:1}
div.content-wrapper{max-width:none}
@media (min-width:1024px){div.content-wrapper{margin-left:auto;margin-right:auto}}
div.content{flex-grow:1;display:flex;flex-direction:column;overflow:auto;padding:.5rem;margin-bottom:2.5rem}
@media (min-width:1024px){div.content{padding:1rem;margin-bottom:0}}
/* Blueprint content area sizing - fluid width, constrained by viewport */
div.content{width:100%;max-width:95%;margin-left:auto;margin-right:auto;padding:1.5rem 2rem;box-sizing:border-box}
div.centered{display:flex;flex-direction:column;flex-wrap:wrap;align-items:center;justify-content:space-around;min-width:100%;margin:0 auto}
div.flushleft,div.raggedright{display:flex;justify-content:flex-start}
div.flushright,div.raggedbottom,div.raggedleft{display:flex;justify-content:flex-end}
div.raggedbottom{flex-direction:column}
div.content{line-height:1.4rem}
div.content>p{margin:2.1rem 0}
li>p{margin:.28rem 0}
.icon{display:inline-block;-webkit-user-select:none;-moz-user-select:none;user-select:none;width:1rem;height:1rem;stroke-width:0;stroke:currentColor;fill:currentColor}
h1,h2,h3,h4,h5,h6{font-family:Lucida Grande,Arial,Helvetica,sans-serif}
h1{font-size:2rem;line-height:2rem;margin:1rem 0}
h1,h2{color:var(--sbs-heading)}
h2{font-size:1.5rem;margin:.8rem 0}
h3,h4{margin:.67rem 0;color:var(--sbs-heading)}
h3,h4,p{font-size:1rem}
p{margin:.5rem 0}
.titlepage{text-align:center}
.titlepage h1{font-weight:400}
b,strong{font-weight:700}
dfn{font-style:italic}
code,kbd,pre,samp{font-family:monospace,serif;font-size:1rem}
pre{white-space:pre-wrap;max-width:100%;overflow-x:auto}
q{quotes:""" """ "'" "'"}
small{font-size:80%}
sub,sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}
sup{top:-.5rem}
sub{bottom:-.25rem}
.mdseries,.textmf{font-weight:400}
.bfseries,.textbf{font-weight:700}
.rmfamily,.textrm{font-family:serif}
.sffamily,.textsf{font-family:sans-serif}
.texttt,.ttfamily{font-family:monospace}
.textup,.upshape{text-transform:uppercase}
.itshape,.textit{font-style:italic}
.slshape,.textsl{font-style:oblique}
.scshape,.textsc{font-variant:small-caps}
small.tiny{font-size:x-small}
small.scriptsize{font-size:smaller}
small.footnotesize,small.small{font-size:small}
.normalsize{font-size:normal}
big.large{font-size:large}
big.xlarge,big.xxlarge{font-size:x-large}
big.huge,big.xhuge{font-size:xx-large}
.rm{font-family:serif;font-style:normal;font-weight:400}
.cal,.it{font-style:italic}
.cal,.it,.sl{font-family:serif;font-weight:400}
.sl{font-style:oblique}
.bf{font-family:serif;font-weight:700}
.bf,.tt{font-style:normal}
.tt{font-family:monospace;font-weight:400}
.underbar{text-decoration:underline}
.fbox,.framebox{border:1px solid var(--sbs-text);padding:1px 3px}
.quotation p,.quote p,.verse p{margin-top:0;margin-bottom:.5em}
hr{color:var(--sbs-border)}
dd{margin-left:3rem}
dd p{padding:0;margin:0 0 1rem}
ul.breadcrumbs{margin:0;padding:0;list-style:none;font-size:small}
ul.breadcrumbs li{display:inline}
ul.breadcrumbs a{text-decoration:none;color:var(--sbs-accent)}
li.crumb:after{content:" / "}
div.equation{display:flex;align-items:center;margin:1rem}
div.equation span.equation_label{margin-right:1rem}
div.equation span.equation_label:before{content:"("}
div.equation span.equation_label:after{content:")"}
div.equation div.equation_content{margin:auto}
figure{display:flex;flex-direction:column;vertical-align:bottom;overflow:auto}
figure img{display:block;margin:0 auto}
figcaption{display:block;text-align:center;margin-bottom:.1rem}
span.caption_ref,span.caption_title,span.subcaption{font-weight:700}
span.caption_ref:after{content:":"}
span.subref:after{content:")"}
footer#footnotes{clear:both;padding-top:1rem;padding-left:1rem;border-color:var(--sbs-border);border-top:1px solid}
footer#footnotes h1{font-size:1.5rem;margin:0;margin-bottom:.5rem;color:var(--sbs-text)}
a.footnote{text-decoration:none}
a.footnote sup:after{content:"]"}
a.footnote sup:before{content:"["}
body>header{display:none;background:linear-gradient(180deg,var(--sbs-accent) 0,var(--sbs-accent));color:#fff;align-items:center;padding:.5rem}
#toc-toggle{font-size:1.75rem;margin-right:1rem;cursor:pointer;color:#fff;display:none}
@media (max-width:1023px){#toc-toggle{display:inline-block}}
h1#doc_title{color:#fff;font-size:1.5rem;margin:auto}
#doc_title a,#doc_title a:visited{text-decoration:none;color:#fff}
.theindex li{list-style-type:none}
nav.index-groups{margin-bottom:1rem}
a[class^=index-group]{text-decoration:none}
a.index-group:after{content:" |"}
section.theindex{display:flex;flex-direction:row;flex-wrap:wrap;margin-top:1rem}
section.theindex h2{min-width:100%;margin:1rem 0 .5rem}
ul.index-column{min-width:100%}
@media (min-width:1024px){ul.index-column{min-width:auto}}
nav.prev_up_next a.index{font-size:small;padding-left:.5rem;padding-right:.5rem}
dl.description dt{font-weight:700}
table.list{margin-left:15px;margin-top:1em;margin-bottom:1em}
table.list td{padding-right:5px}
div.displaymath{overflow:auto}
a.eqref:before{content:"("}
a.eqref:after{content:")"}
nav.prev_up_next{position:fixed;z-index:1;right:0;bottom:0;display:flex;height:2.5rem;background:linear-gradient(180deg,var(--sbs-accent) 0,var(--sbs-accent))}
nav.prev_up_next a{font-size:150%;margin:auto;padding:.5rem 1rem;text-decoration:none;color:#fff;text-shadow:1px 2px 0 rgba(0,0,0,.8)}
hspace,vspace{margin:0;padding:0}
div.bigskip{margin-bottom:4rem}
div.medskip{margin:0;padding:0;margin-bottom:2rem}
div.bigskip{margin:0;padding:0;margin-bottom:1rem}
.tabular{border-collapse:collapse;color:var(--sbs-text);background-color:var(--sbs-bg-page);width:auto}
.tabular td,.tabular th{vertical-align:baseline;text-align:left;padding:.3em .6em;empty-cells:show}
td p:first-child,th p:first-child{margin-top:0;margin-bottom:0}
td p,th p{margin-top:1em;margin-bottom:0}
@keyframes a{0%{background-color:var(--sbs-border)}to{background-color:var(--sbs-bg-page)}}
div[class$=_thmwrapper]{margin-top:1rem}
div[class$=_thmwrapper]:target{animation:a 1s ease}
div[class$=_thmheading]{display:flex;font-weight:700;line-height:150%}
span[class$=_thmtitle]:before{content:"("}
span[class$=_thmtitle]:after{content:")"}
div[class$=_thmcontent]{font-weight:400;margin-left:1rem;padding-top:.14rem;padding-left:1rem}
span[class$=_thmlabel]{margin-left:.5rem;margin-right:.5rem}
div[class$=proof_heading]{font-weight:700;line-height:120%;cursor:pointer}
div.proof_content{font-weight:400;margin-left:1rem;padding-top:.5rem;padding-left:1rem}
span.expand-proof{font-size:80%}
div.hilite{animation:a 1s ease}
span.qed{float:right}
/* Old plasTeX modal styles removed - now using .dep-modal-* from common.css */
a.icon{text-decoration:none;color:var(--sbs-text);border:none;background-color:Transparent}
div[class$=_thmheading]:hover div.thm_header_hidden_extras{display:inline-block}
div.thm_header_hidden_extras{display:none}
ul.quizz{display:flex;flex-direction:column;list-style:circle!important}
ul.quizz li{display:flex;padding:.5rem;flex-direction:row;min-width:100%;min-height:3rem;flex-grow:1;align-items:center;justify-content:space-between}
ul.quizz li.active-qright{background-color:green}
ul.quizz li.active-qwrong{background-color:red}
ul.quizz svg.icon{display:none;padding-right:.5rem;width:2rem;height:2rem}
.tikzcd{overflow:auto}
.tikzcd,.tikzpicture{display:block;margin:.5rem auto}
.local_toc ul{padding-left:1rem;list-style:none}
.local_toc ul a{text-decoration:none;color:var(--sbs-text)}
.local_toc ul li{padding:.2rem 0}
nav.toc{flex-shrink:0;display:none;width:100%;height:100%;overflow-x:hidden;overflow-y:auto;flex-direction:column;margin-right:1rem;padding:0;padding-right:1rem;transition:left .5s ease;background-color:var(--sbs-accent);border-right:none}
@media (min-width:1024px){nav.toc{display:flex;max-width:27ch}}
nav.active{width:100%}
.toc ul{min-width:100%;padding-left:0;list-style:none}
.toc ul .sidebar-item{display:inline-block;padding:.35rem .8rem;transition:all .1s ease;text-align:left;text-decoration:none;font-size:0.875rem;line-height:1.4;color:#fff;flex-grow:1;white-space:nowrap}
.toc ul a:hover{transition:all .2s ease;background:var(--sbs-accent)}
.toc .nav-separator {
  height: 1px;
  background-color: rgba(255,255,255,0.3);
  margin: 0.5rem 0.75rem;
  list-style: none;
}
.toc ul li{display:flex;min-width:100%;align-items:center;flex-wrap:wrap;justify-content:space-between;background-color:var(--sbs-accent)}
.toc ul li.sidebar-blueprint-group{align-items:stretch}
.toc ul li.current{background-color:rgba(255, 255, 255, 0.2);font-weight:400}
.sub-toc-0 .sidebar-item{padding-left:.8rem}
.sub-toc-1 .sidebar-item{padding-left:1.6rem}
.sub-toc-2 .sidebar-item{padding-left:2.4rem}
.sub-toc-3 .sidebar-item{padding-left:3.2rem}
.sub-toc-4 .sidebar-item{padding-left:4rem}
ul.sub-toc-1,ul.sub-toc-2,ul.sub-toc-3,ul.sub-toc-4{display:none}
span.expand-toc{min-width:.7rem;width:.8rem;height:.8rem;padding:0;padding-right:.5rem;font-size:125%;cursor:pointer;text-align:center;color:#fff;background-color:Transparent}
svg.close-toc{min-width:1.3rem;min-height:1.3rem;margin:.5rem;margin-left:auto;display:none;cursor:pointer;text-align:center;color:#fff;background-color:Transparent}
nav.active svg.close-toc{display:inline-block}
ul.active{display:block}
code.verb{font-family:monospace;font-style:normal;font-weight:400}
pre.verbatim{margin:1rem 2rem;background-color:var(--sbs-bg-surface);padding:.5rem}

/* ========== Side-by-side Layout (from leanblueprint) ========== */

/* Constrain non-node content (paragraphs, lists, display math) to left column width.
   These elements appear in chapter-page, section, and direct content areas.
   45% matches the left column of .sbs-container grid (1fr out of 1fr + 1.2fr).
   80ch caps readability on any screen size. */
.chapter-page > p,
.chapter-page > div.displaymath,
.chapter-page > ul,
.chapter-page > ol,
.chapter-page > blockquote,
section.section > p,
section.section > div.displaymath,
section.section > ul,
section.section > ol,
section.section > blockquote,
div.content > p,
div.content > div.displaymath,
div.content > ul:not(.chapter-index):not(.dashboard-list):not(.notes-list):not(.toc),
div.content > ol,
div.content > blockquote {
  max-width: min(45%, 80ch);
}

/* Allow wide equations to scroll within the constrained width */
.chapter-page > div.displaymath,
section.section > div.displaymath,
div.content > div.displaymath {
  overflow-x: auto;
}

a.github_link {
  font-weight: normal;
  font-size: 90%;
  text-decoration: none;
  color: inherit;
}

/* Note: .sbs-container grid layout is defined in common.css
   This section only adds blueprint-specific spacing */
.sbs-container {
  margin-bottom: 3rem;
}

/* Grid cell styles for 5-row layout (above, heading, statement, proof, below) */
.sbs-signature pre.lean-code,
.sbs-proof-lean pre.lean-code {
  margin: 0;
  font-family: 'JetBrains Mono', 'Fira Code', monospace;
  font-size: 0.85rem;
  line-height: 1.5;
  white-space: pre;
  max-width: 100%;
  overflow-x: auto;
}

/* Align Lean proof body top with LaTeX proof body top.
   The LaTeX column has a proof_wrapper (margin-top 0.75rem) + proof_heading (~1.2rem)
   + proof_content margin/padding (~0.75rem) + first <p> margin (1rem).
   Total offset ~4.3rem from grid cell top to first proof text line. */
.sbs-proof-lean pre.lean-code {
  padding-top: 2.9rem;
}

.sbs-signature pre.lean-code code,
.sbs-proof-lean pre.lean-code code {
  font-family: inherit;
}

.sbs-signature {
  position: relative;
}

/* Legacy column classes (kept for dep graph modals and Verso fallback) */
.sbs-latex-column {
  overflow-wrap: break-word;
  word-wrap: break-word;
}

.sbs-lean-column {
  min-width: 0;
  max-width: 100%;
  overflow-x: auto;
  position: relative;
}

.sbs-lean-column pre.lean-code {
  margin: 0;
  padding-top: 1.5rem;
  background-color: var(--sbs-bg-surface);
  font-family: 'JetBrains Mono', 'Fira Code', monospace;
  font-size: 0.85rem;
  line-height: 1.5;
  white-space: pre;
  max-width: 100%;
  overflow-x: auto;
}

.sbs-lean-column pre.lean-code code {
  font-family: inherit;
}

.lean-github-hover {
  position: absolute;
  top: 0;
  right: 0;
  opacity: 0;
  transition: opacity 0.2s;
  padding: 0.25rem;
  color: var(--sbs-text-muted);
}

.lean-github-hover:hover {
  color: var(--sbs-link);
}

.sbs-lean-column:hover .lean-github-hover,
.sbs-signature:hover .lean-github-hover {
  opacity: 1;
}

.thm_body_extras {
  display: none;
}

.proof_wrapper.proof_inline {
  display: block !important;
}

.proof_wrapper.proof_inline .proof_content {
  display: none;
}

/* ========== Multi-page Navigation ========== */
.prev-next-nav {
  display: flex;
  justify-content: space-between;
  align-items: center;
  margin-top: 3rem;
  padding-top: 1.5rem;
  border-top: 1px solid var(--sbs-border);
}

.prev-next-nav a {
  color: var(--sbs-accent);
  text-decoration: none;
  padding: 0.5rem 1rem;
  border: 1px solid var(--sbs-border);
  border-radius: 4px;
  transition: background-color 0.2s;
}

.prev-next-nav a:hover {
  background-color: var(--sbs-bg-surface);
}

.prev-next-nav a.prev {
  margin-right: auto;
}

.prev-next-nav a.next {
  margin-left: auto;
}

/* Chapter list on index page */
.chapter-list {
  margin: 2rem 0;
}

.chapter-list h2 {
  margin-bottom: 1rem;
  color: var(--sbs-heading);
}

.chapter-index {
  padding-left: 1.5rem;
}

.chapter-index li {
  margin: 0.5rem 0;
  line-height: 1.6;
}

.chapter-index a {
  color: var(--sbs-accent);
  text-decoration: none;
}

.chapter-index a:hover {
  text-decoration: underline;
}

/* Chapter page styling */
.chapter-page {
  margin: 1rem 0;
}

.chapter-title {
  color: var(--sbs-heading);
  margin-bottom: 1.5rem;
}

.chapter-nodes, .section-nodes {
  margin: 1rem 0;
}

.section {
  margin: 2rem 0;
  padding-top: 1rem;
  border-top: 1px solid var(--sbs-border);
}

.section-title {
  color: var(--sbs-heading);
  margin-bottom: 1rem;
}

/* Active sidebar item highlighting */
nav.toc li.active a {
  background-color: var(--sbs-accent);
  font-weight: bold;
}

/* ========== Blueprint Theme Styles (from Theme.lean) ========== */
/* Legacy --bp-* variables mapped to --sbs-* for backwards compatibility */
:root {
  --bp-primary: var(--sbs-link);
  --bp-success: var(--sbs-success);
  --bp-warning: var(--sbs-warning);
  --bp-danger: var(--sbs-danger);
  --bp-muted: var(--sbs-text-muted);
  --bp-bg: var(--sbs-bg-surface);
  --bp-bg-alt: var(--sbs-bg-surface);
  --bp-border: var(--sbs-border);
  --bp-text: var(--sbs-text);
  --bp-text-muted: var(--sbs-text-muted);
  --bp-font-sans: system-ui, -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, sans-serif;
  --bp-font-mono: ui-monospace, SFMono-Regular, 'SF Mono', Menlo, Monaco, Consolas, monospace;
  --bp-max-width: 1200px;
  --bp-spacing: 1.5rem;
}

/* Progress Section */
.progress-section {
  margin: 2rem 0;
  padding: 1rem 0;
}

/* Stats Box - matches dep-graph-legend styling */
.stats-box {
  background: var(--sbs-bg-surface);
  border: 1px solid var(--sbs-border);
  border-radius: 8px;
  min-width: 340px;
  height: 500px;
  overflow: hidden;
  font-size: 0.875rem;
  color: var(--sbs-text);
}

.stats-title {
  font-weight: bold;
  text-align: center;
  padding: 0.75rem 0.5rem;
  font-size: 1.25rem;
}

.stats-separator {
  width: calc(100% - 1.5rem);  /* Leave 0.75rem gap on each side */
  margin: 0 auto;  /* Center it */
  height: 1px;
  background-color: var(--sbs-border);
}

.stats-main {
  display: flex;
  align-items: center;
  justify-content: center;
  padding: 1rem;
  gap: 1.5rem;
}

.stats-pie-container {
  flex-shrink: 0;
}

.stats-pie {
  width: 180px;
  height: 180px;
}

.stats-legend-separator {
  display: none;
}

.stats-legend {
  display: flex;
  flex-direction: column;
  justify-content: center;
  gap: 0.35rem;
}

.stats-legend .legend-item {
  display: flex;
  align-items: center;
  gap: 0.5rem;
}

.stats-legend .legend-swatch {
  width: 16px;
  height: 16px;
  border-radius: 3px;
  flex-shrink: 0;
}

/* Color classes for stats legend - use unified status colors (7 statuses) */
.stats-legend .legend-swatch.not-ready { background-color: var(--sbs-status-not-ready); }
.stats-legend .legend-swatch.wip { background-color: var(--sbs-status-wip); }
.stats-legend .legend-swatch.sorry { background-color: var(--sbs-status-sorry); }
.stats-legend .legend-swatch.proven { background-color: var(--sbs-status-proven); }
.stats-legend .legend-swatch.fully-proven { background-color: var(--sbs-status-fully-proven); }
.stats-legend .legend-swatch.mathlib-ready { background-color: var(--sbs-status-mathlib-ready); }
.stats-legend .legend-swatch.axiom { background-color: var(--sbs-status-axiom); }

.stats-summary {
  padding: 0.75rem;
  text-align: center;
  min-height: calc(150px + 1.5rem);  /* Match pie height + stats-main padding */
  box-sizing: border-box;
  display: flex;
  flex-direction: column;
  justify-content: center;
  gap: 0.5rem;
}

.stats-total {
  font-size: 0.875rem;
  font-weight: normal;
  color: var(--sbs-text);
}

.stats-percentages {
  font-size: 0.875rem;
  color: var(--sbs-text-muted);
}

/* Dashboard Grid Layout */
.dashboard-grid {
  display: flex;
  flex-direction: column;
  gap: 1rem;
  margin-bottom: 2rem;
  width: 100%;
}

/* Top row: Progress (fixed width) + Key Theorems (fills remaining space) */
.dashboard-row.top-row {
  display: flex;
  gap: 1rem;
  align-items: flex-start;  /* Don't stretch to match heights */
}

/* Bottom row: Spacer (matches progress-cell) + Project Notes (fills remaining like key-declarations) */
.dashboard-row.bottom-row {
  display: flex;
  width: 100%;
  min-height: 200px;
  gap: 1rem;
  align-items: flex-start;  /* Don't stretch to match heights */
}

/* Invisible spacer to align Project Notes with Key Declarations */
.dashboard-row.bottom-row::before {
  content: '';
  flex-shrink: 0;
  min-width: 400px;  /* Match progress-cell width */
  max-width: 575px;
}

/* Ensure notes cell fills available height */
.dashboard-row.bottom-row .dashboard-cell.notes-cell {
  flex: 1;
  display: flex;
  flex-direction: column;
}

.dashboard-row.bottom-row .stats-box.project-notes {
  flex: 1;
  min-height: 200px;
}

.dashboard-cell {
  min-height: 200px;
}

/* Progress stats box - fixed size, don't stretch */
.dashboard-cell.progress-cell {
  flex-shrink: 0;
  min-width: 400px;
  max-width: 575px;
  width: auto;
  word-wrap: break-word;
  overflow-wrap: break-word;
}

/* Key theorems fills remaining space */
.dashboard-cell.key-declarations-cell {
  flex: 1;
  min-width: 0;  /* Allow shrinking */
}

/* Notes cell spans full width */
.dashboard-cell.notes-cell {
  width: 100%;
}

/* Make all stats boxes in dashboard have same styling */
.stats-box.key-declarations,
.stats-box.project-notes {
  background: var(--sbs-bg-surface);
  border: 1px solid var(--sbs-border);
  border-radius: 8px;
  font-size: 0.875rem;
  color: var(--sbs-text);
  height: 100%;
  display: flex;
  flex-direction: column;
  width: auto;  /* Override fixed width from base stats-box */
}

/* Gap between key declarations and project notes (matches checks-tile margin) */
.stats-box.project-notes {
  margin-top: 1rem;
}

/* Dashboard list styling */
.dashboard-list {
  list-style: none;
  padding: 0;
  margin: 0.75rem;
  overflow-y: auto;
  flex-grow: 1;
}

.dashboard-list li {
  margin-bottom: 0.5rem;
  line-height: 1.4;
}

.dashboard-list a,
.dashboard-list a:visited {
  color: var(--sbs-text-muted);
  text-decoration: none;
}

.dashboard-list a:hover {
  color: var(--sbs-text);
  text-decoration: underline;
  text-underline-offset: 2px;
}

/* Message and note text styling */
.message-text,
.note-text {
  color: var(--sbs-text-muted);
  font-style: italic;
}

/* Empty state */
.stats-empty {
  padding: 0.75rem;
  color: var(--sbs-text-muted);
  font-style: italic;
  text-align: center;
  flex-grow: 1;
  display: flex;
  align-items: center;
  justify-content: center;
}

/* Notes content - multi-column layout */
.notes-content {
  padding: 0.75rem;
  overflow-y: auto;
  flex-grow: 1;
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(280px, 1fr));
  gap: 0.75rem;
  align-items: start;
}

.note-section {
  margin-bottom: 0.5rem;
  background: var(--sbs-bg-surface);
  border-radius: 4px;
  padding: 0.75rem;
}

.note-section:last-child {
  margin-bottom: 0;
}

.note-section h4 {
  margin: 0 0 0.5rem 0;
  padding-bottom: 0.35rem;
  border-bottom: 1px solid var(--sbs-border);
  font-size: 0.8rem;
  font-weight: 600;
  color: #0000ff;  /* Lean keyword blue (light mode) */
  text-transform: uppercase;
  letter-spacing: 0.5px;
}

/* Dark mode: brighter blue for Lean keyword style headers */
html[data-theme="dark"] .note-section h4 {
  color: #569cd6;
}

.note-section ul {
  margin: 0;
  padding-left: 0;
}

/* Responsive: stack on mobile */
@media (max-width: 768px) {
  .dashboard-row.top-row {
    flex-direction: column;
  }

  .dashboard-cell.progress-cell {
    width: 100%;
  }

  .dashboard-cell {
    min-height: 150px;
  }
}

/* Ultra-wide screens (4K/5K) - more breathing room */
@media (min-width: 2560px) {
    div.content {
        padding: 2rem 3rem;
    }
    .sbs-container {
        gap: 0.75rem 1.5rem;
    }
}

/* ===================== */
/* Dashboard Phase 2 CSS */
/* ===================== */

/* Double progress panel width */
.progress-cell {
  min-width: 400px;
}

/* Key declaration previews */
.key-declarations-list {
  display: flex;
  flex-direction: column;
  gap: 0;
  padding: 0 0.75rem;  /* Consistent padding with other lists */
}

.key-declaration-item {
  display: flex;
  align-items: flex-start;
  gap: 0.75rem;
  padding: 0.75rem 0.5rem;
  border-bottom: 1px solid var(--sbs-border);
  width: 100%;
}

.key-declaration-item:last-child {
  border-bottom: none;
}

/* Key declarations uniform styling */
.key-declaration-item {
  background-color: var(--sbs-bg-surface);
  border-radius: 4px;
}

/* Key declaration status dot positioning */
.key-declaration-item .status-dot {
  margin-top: 0.5rem;
}

.key-declaration-link,
.key-declaration-link:visited,
.key-declaration-link:hover,
.key-declaration-link:active {
  flex: 1;
  text-decoration: none;
  color: inherit;
}

.key-declaration-title-link,
.key-declaration-title-link:visited {
  color: var(--sbs-link);
  text-decoration: none;
  font-weight: 600;
  display: block;
  margin-bottom: 0.5rem;
}

.key-declaration-title-link:hover {
  color: var(--sbs-link-hover);
  text-decoration: underline;
  text-underline-offset: 2px;
}

.key-declaration-preview {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 0.75rem;
  font-size: 0.8rem;
  cursor: text;
  user-select: text;
}

.kd-latex,
.kd-lean {
  overflow: visible;
}

.kd-env {
  font-weight: 600;
  color: var(--sbs-text);
}

.kd-label {
  color: var(--sbs-text-muted);
}

.kd-statement {
  margin-top: 0.25rem;
  color: var(--sbs-text);
}

.kd-lean code {
  font-size: 0.75rem;
  background: transparent;
  padding: 0.25rem;
  border-radius: 3px;
  display: block;
  overflow: hidden;
}

.kd-lean pre.lean-code {
  font-size: 0.75rem;
  background: transparent;
  padding: 0.25rem;
  border-radius: 3px;
  margin: 0;
  overflow: visible;
}

.kd-lean pre.lean-code code {
  font-size: inherit;
  background: transparent;
  padding: 0;
}

/* Stats details structured layout (compacted for larger pie chart) */
.stats-details {
  padding: 0.5rem 1rem;
}

.stats-details .stats-total {
  text-align: center;
  font-size: 0.95rem;
  font-weight: 600;
  margin-bottom: 0.5rem;
  color: var(--sbs-text);
}

.stats-details .stats-columns {
  display: flex;
  justify-content: space-evenly;
  gap: 1.5rem;
}

.stats-details .stats-column {
  width: 130px;
}

.stats-details .stats-column-header {
  text-align: center;
  font-weight: 600;
  text-transform: uppercase;
  font-size: 0.7rem;
  margin-bottom: 0.5rem;
  color: var(--sbs-text-muted);
}

.stats-details .stats-row {
  display: flex;
  justify-content: space-between;
  font-size: 0.8rem;
  padding: 0.15rem 0;
  line-height: 1.4;
}

.stats-details .stats-value {
  text-align: right;
  min-width: 35px;
  font-weight: 600;
  font-variant-numeric: tabular-nums;
}

.stats-details .stats-label {
  text-align: left;
  color: var(--sbs-text-muted);
}

/* Project Notes two-column layout */
.notes-layout {
  display: flex;
  flex-direction: row;
  gap: 1.5rem;
  padding: 0.75rem;
}

.notes-messages,
.notes-other {
  flex: 1;
  min-width: 0;
}

/* Messages column: padding from left edge + vertical divider on right */
.notes-messages {
  padding-left: 0.5rem;
  padding-right: 1.5rem;
  border-right: 1px solid var(--sbs-border);
}

/* Messages header: same blue styling as note-section headers */
.notes-messages h4 {
  margin: 0 0 0.5rem 0;
  padding-bottom: 0.35rem;
  border-bottom: 1px solid var(--sbs-border);
  font-size: 0.8rem;
  font-weight: 600;
  color: #0000ff;  /* Lean keyword blue (light mode) */
  text-transform: uppercase;
  letter-spacing: 0.5px;
}

/* Dark mode: brighter blue for Messages header */
html[data-theme="dark"] .notes-messages h4 {
  color: #569cd6;
}

/* Other notes column: padding from the vertical divider */
.notes-other {
  padding-left: 0.5rem;
}

.notes-list {
  list-style: none;
  padding: 0;
  margin: 0;
}

.notes-list li {
  margin-bottom: 0.5rem;
  line-height: 1.4;
}

.notes-list a {
  color: var(--sbs-text-muted);
  text-decoration: none;
}

.notes-list a:hover {
  color: var(--sbs-text);
  text-decoration: underline;
}

.note-content {
  color: var(--sbs-text);
  font-size: 0.875rem;
}

.notes-empty {
  color: var(--sbs-text-muted);
  font-style: italic;
  text-align: center;
  padding: 1rem;
}

.note-section .dashboard-list {
  margin: 0;
  padding-left: 1rem;
}

.note-section .dashboard-list li {
  margin-bottom: 0.25rem;
}

.note-text {
  color: var(--sbs-text-muted);
  font-size: 0.85rem;
}

/* ========================================
   Checks Tile (Dashboard)
   ======================================== */

.checks-tile {
  background-color: var(--sbs-bg-surface);
  border: 1px solid var(--sbs-border);
  border-radius: 8px;
  padding: 0;  /* Match stats-box padding (handled by children) */
  margin-top: 1rem;
  box-sizing: border-box;
}

.checks-tile h3 {
  margin: 0 0 0.75rem 0;
  padding-bottom: 0.5rem;
  border-bottom: 1px solid var(--sbs-border);
  font-size: 1.1rem;
  color: var(--sbs-text);
}

.checks-list {
  display: flex;
  flex-direction: column;
  gap: 0.5rem;
  padding: 0.75rem;
}

.check-item {
  display: flex;
  align-items: center;
  gap: 0.5rem;
  padding: 0.5rem 0.75rem;
  border-radius: 4px;
  font-size: 0.9rem;
}

.check-item.check-pass {
  background-color: var(--sbs-check-pass-bg);
  border-left: 3px solid var(--sbs-success);
}

.check-item.check-fail {
  background-color: var(--sbs-check-fail-bg);
  border-left: 3px solid var(--sbs-danger);
}

.check-icon {
  font-weight: bold;
  font-size: 1.1rem;
}

.check-pass .check-icon {
  color: var(--sbs-success);
}

.check-fail .check-icon {
  color: var(--sbs-danger);
}

.check-text {
  color: var(--sbs-text);
  overflow-wrap: break-word;
  word-wrap: break-word;
  min-width: 0;
}

.cycles-detail {
  margin-top: 0.5rem;
  padding-left: 1.5rem;
}

.cycles-detail ul {
  margin: 0;
  padding-left: 1rem;
  font-size: 0.85rem;
  color: var(--sbs-text-muted);
}

.cycles-detail li {
  margin: 0.25rem 0;
  font-family: monospace;
}

/* Dark mode: uses CSS variables defined in html[data-theme="dark"] in common.css */
html[data-theme="dark"] .check-item.check-pass {
  background-color: var(--sbs-check-pass-bg);
}

html[data-theme="dark"] .check-item.check-fail {
  background-color: var(--sbs-check-fail-bg);
}

.check-item.check-pending {
  background: var(--sbs-bg-surface);
  border-left: 4px solid var(--sbs-border);
  opacity: 0.6;
}

.check-pending .check-icon {
  color: var(--sbs-text-muted);
}

.check-pending .check-status {
  font-size: 0.8rem;
  color: var(--sbs-text-muted);
  margin-left: auto;
}

/* Warning state for checks (e.g., partial coverage) */
.check-item.check-warn {
  background-color: var(--sbs-check-warn-bg);
  border-left: 3px solid var(--sbs-warning);
}

.check-warn .check-icon {
  color: var(--sbs-warning);
}

html[data-theme="dark"] .check-item.check-warn {
  background-color: var(--sbs-check-warn-bg);
}

/* Coverage detail list (mirrors cycles-detail) */
.coverage-detail {
  margin-top: 0.5rem;
  padding-left: 1.5rem;
}

.coverage-detail ul {
  margin: 0;
  padding-left: 1rem;
  font-size: 0.85rem;
  color: var(--sbs-text-muted);
}

.coverage-detail li {
  margin: 0.25rem 0;
  font-family: monospace;
}

/* === Axiom Page Sections === */
.axiom-section {
  margin-bottom: 1.5rem;
}

.axiom-section-header {
  display: flex;
  align-items: center;
  gap: 0.5rem;
  padding: 0.75rem 1rem;
  font-weight: 600;
  font-size: 1rem;
  border-radius: 4px 4px 0 0;
}

.axiom-section-standard .axiom-section-header {
  border-left: 3px solid var(--sbs-success);
  background-color: var(--sbs-check-pass-bg);
}

.axiom-section-project .axiom-section-header {
  border-left: 3px solid var(--sbs-status-axiom);
  background-color: var(--sbs-check-warn-bg);
}

/* Legacy progress bar styles (kept for backwards compatibility) */
.progress-bar {
  height: 8px;
  background: var(--bp-border);
  border-radius: 4px;
  overflow: hidden;
  margin: 0.75rem 0;
}

.progress-fill {
  height: 100%;
  background: var(--bp-primary);
  transition: width 0.3s ease;
}

.progress-label {
  font-size: 0.8125rem;
  color: var(--bp-text-muted);
  text-align: right;
  margin-top: 0.25rem;
}

.progress-stats {
  display: flex;
  flex-wrap: wrap;
  gap: 0.25rem 1rem;
  align-items: center;
  font-size: 0.8125rem;
  color: var(--bp-text-muted);
}

.stat {
  display: inline-flex;
  align-items: center;
  gap: 0.375rem;
}

.stat::before {
  content: '';
  display: inline-block;
  width: 8px;
  height: 8px;
  border-radius: 2px;
  flex-shrink: 0;
}

.stat.proved::before { background: var(--bp-success); }
.stat.mathlib::before { background: var(--bp-primary); }
.stat.not-ready::before { background: var(--bp-danger); }
.stat.total::before { background: var(--bp-text-muted); }

.stat-separator {
  color: var(--bp-border);
  margin: 0 0.25rem;
}

/* Node Styles */
.node {
  border: 1px solid var(--bp-border);
  border-radius: 8px;
  margin: 1.5rem 0;
  overflow: hidden;
}

.node-header {
  display: flex;
  align-items: center;
  gap: 0.75rem;
  padding: 1rem;
  background: var(--bp-bg-alt);
  border-bottom: 1px solid var(--bp-border);
}

.node-env {
  font-weight: 600;
  text-transform: capitalize;
}

.node-title {
  flex: 1;
}

.node-status {
  width: 12px;
  height: 12px;
  border-radius: 50%;
}

/* Legacy 4-status classes removed (#340) - old model used proved/mathlib-ok/stated/not-ready */

.node-content {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 1rem;
  padding: 1rem;
}

@media (max-width: 768px) {
  .node-content {
    grid-template-columns: 1fr;
  }
}

.node-statement, .node-proof {
  padding: 1rem;
  background: var(--bp-bg-alt);
  border-radius: 4px;
}

.node-statement h4, .node-proof h4 {
  margin: 0 0 0.75rem 0;
  font-size: 0.875rem;
  color: var(--bp-text-muted);
  text-transform: uppercase;
  letter-spacing: 0.05em;
}

.node-footer {
  padding: 0.75rem 1rem;
  border-top: 1px solid var(--bp-border);
  font-size: 0.875rem;
  color: var(--bp-text-muted);
}

.node-decls, .node-deps {
  display: inline;
}

.node-decls + .node-deps::before {
  content: " | ";
  margin: 0 0.5rem;
}

.decl-link, .dep-link {
  color: var(--bp-primary);
  text-decoration: none;
}

.decl-link:hover, .dep-link:hover {
  text-decoration: underline;
}

/* Index Page */
.index-header {
  text-align: center;
  margin-bottom: 2rem;
}

.index-header h1 {
  margin-bottom: 1rem;
}

.github-link, .docs-link {
  margin: 0 0.5rem;
  color: var(--bp-primary);
}

/* Note: Graph section, viewport, and toolbar styles moved to dep_graph.css */

/* Node Lists */
.node-lists {
  margin: 2rem 0;
}

.node-list h3 {
  margin-bottom: 1rem;
}

.node-index {
  list-style: none;
  padding: 0;
  margin: 0;
}

.node-index li {
  padding: 0.5rem 0;
  border-bottom: 1px solid var(--bp-border);
}

.node-index a {
  color: var(--bp-text);
  text-decoration: none;
  display: flex;
  align-items: center;
  gap: 0.5rem;
}

.node-index a:hover {
  color: var(--bp-primary);
}

/* Lean Code Highlighting */
pre.lean-code {
  font-family: var(--bp-font-mono);
  font-size: 0.875rem;
  padding: 1rem;
  overflow-x: auto;
  background: var(--bp-bg);
}

/* Math rendering */
.math.inline { }
.math.display {
  overflow-x: auto;
  padding: 1rem 0;
}

/* Note: Full-page graph, legend, modals, and SBS container in modal styles moved to dep_graph.css */

/* ========== Paper-Like Typography for TeX Blueprint Pages ========== */
/* Issue #49: Visual differentiation between TeX and Verso blueprint pages.
   TeX pages should feel like reading a typeset paper. */

/* Base typography for chapter pages */
.chapter-page {
  font-family: Georgia, "Palatino Linotype", "Book Antiqua", Palatino, serif;
  line-height: 1.7;
  text-align: justify;
  -webkit-hyphens: auto;
  hyphens: auto;
}

/* Serif headings for chapter pages */
.chapter-page h1,
.chapter-page h2,
.chapter-page h3,
.chapter-page h4,
.chapter-page h5,
.chapter-page h6 {
  font-family: Georgia, "Palatino Linotype", "Book Antiqua", Palatino, serif;
  text-align: left; /* Headings stay left-aligned even with justified body */
}

/* Narrower prose column for paper-like feel - matches left column of SBS grid */
.chapter-page > p,
.chapter-page > div.displaymath,
.chapter-page > ul,
.chapter-page > ol,
.chapter-page > blockquote {
  max-width: min(45%, 80ch);
}

/* Also narrow section content */
.chapter-page section.section > p,
.chapter-page section.section > div.displaymath,
.chapter-page section.section > ul,
.chapter-page section.section > ol,
.chapter-page section.section > blockquote {
  max-width: min(45%, 80ch);
}

/* More generous paragraph spacing */
.chapter-page p {
  margin: 1rem 0;
}

/* Theorem environments - italic statements (math paper convention) */
.chapter-page div[class$=_thmcontent] {
  font-style: italic;
}

/* Definition bodies should stay roman (upright) */
.chapter-page .definition_thmcontent,
.chapter-page .notation_thmcontent,
.chapter-page .remark_thmcontent,
.chapter-page .example_thmcontent {
  font-style: normal;
}

/* Section dividers - lighter, more paper-like */
.chapter-page .section {
  border-top-color: var(--sbs-border);
  border-top-style: solid;
  border-top-width: 0.5px;
}

/* ========== Simplified Proof Toggle for TeX Pages ========== */
/* Plain [show]/[hide] text instead of modern button style */

.chapter-page .proof_heading {
  background: none;
  border: none;
  border-radius: 0;
  padding: 0;
  box-shadow: none;
  font-weight: normal;
  font-style: italic;
  display: inline;
  gap: 0;
}

.chapter-page .proof_heading:hover {
  background: none;
  border: none;
  box-shadow: none;
}

.chapter-page .proof_heading:active {
  background: none;
}

/* Hide the chevron, replace with [show]/[hide] text */
.chapter-page .expand-proof {
  font-size: 0;
  color: var(--sbs-text);
  transform: none !important; /* Never rotate text */
  display: inline;
}

.chapter-page .expand-proof::before {
  content: '[show]';
  font-size: 0.85rem;
  color: var(--sbs-text);
  text-decoration: underline;
  font-style: normal;
  font-weight: normal;
}

.chapter-page .proof_wrapper.expanded .expand-proof::before {
  content: '[hide]';
}

/* Proof caption styling */
.chapter-page .proof_caption {
  font-style: italic;
  margin-right: 0.25rem;
}

/* Dark mode for paper-like chapter styles */
html[data-theme="dark"] .chapter-page .expand-proof::before {
  color: var(--sbs-text);
}

/* ========== Simplified Proof Toggle for Node Pages (dep_graph) ========== */
/* Same paper-like [show]/[hide] text as chapter pages */

.dg-node-page .proof_heading {
  background: none;
  border: none;
  border-radius: 0;
  padding: 0;
  box-shadow: none;
  font-weight: normal;
  font-style: italic;
  display: inline;
  gap: 0;
}

.dg-node-page .proof_heading:hover {
  background: none;
  border: none;
  box-shadow: none;
}

.dg-node-page .proof_heading:active {
  background: none;
}

/* Hide the chevron, replace with [show]/[hide] text */
.dg-node-page .expand-proof,
.dep-modal-body-wrapper .expand-proof {
  font-size: 0;
  color: var(--sbs-text);
  transform: none !important; /* Never rotate text */
  display: inline;
}

.dg-node-page .expand-proof::before,
.dep-modal-body-wrapper .expand-proof::before {
  content: '[show]';
  font-size: 0.85rem;
  color: var(--sbs-text);
  text-decoration: underline;
  font-style: normal;
  font-weight: normal;
}

.dg-node-page .proof_wrapper.expanded .expand-proof::before,
.dep-modal-body-wrapper .proof_wrapper.expanded .expand-proof::before {
  content: '[hide]';
}

/* Proof caption styling */
.dg-node-page .proof_caption,
.dep-modal-body-wrapper .proof_caption {
  font-style: italic;
  margin-right: 0.25rem;
}

/* Dark mode for node page proof toggle */
html[data-theme="dark"] .dg-node-page .expand-proof::before,
html[data-theme="dark"] .dep-modal-body-wrapper .expand-proof::before {
  color: var(--sbs-text);
}

/* ========== Subgraph Viewport (Node Pages) ========== */

.subgraph-viewport {
  min-height: 120px;
  overflow: auto;
  border: 1px solid var(--sbs-border);
  border-radius: 4px;
  background: var(--sbs-bg-surface);
  padding: 0.5rem;
}

.subgraph-viewport svg {
  display: block;
  margin: 0 auto;
}

.subgraph-viewport svg text {
  font-family: system-ui, -apple-system, sans-serif;
  font-size: 11px;
  fill: var(--sbs-text);
  pointer-events: none;
}

.subgraph-viewport svg .subgraph-node rect,
.subgraph-viewport svg .subgraph-node ellipse {
  stroke: var(--sbs-border);
  stroke-width: 1.5;
  cursor: pointer;
  transition: opacity 0.15s;
}

.subgraph-viewport svg .subgraph-node:hover rect,
.subgraph-viewport svg .subgraph-node:hover ellipse {
  opacity: 0.85;
}

.subgraph-viewport svg .subgraph-target rect,
.subgraph-viewport svg .subgraph-target ellipse {
  stroke-width: 3;
  stroke: var(--sbs-text);
}

.subgraph-viewport svg .subgraph-edge {
  stroke: var(--sbs-text-muted);
  stroke-width: 1;
  fill: none;
}

.subgraph-viewport svg .subgraph-edge-arrow {
  fill: var(--sbs-text-muted);
}

.subgraph-empty {
  text-align: center;
  color: var(--sbs-text-muted);
  font-style: italic;
  padding: 1.5rem;
  font-size: 0.85rem;
}

.subgraph-show-more {
  text-align: center;
  margin-top: 0.5rem;
}

.subgraph-show-more a {
  font-size: 0.8rem;
  color: var(--sbs-link);
  cursor: pointer;
  text-decoration: underline;
}