:root {
  --bg: #ffffff;
  --surface: #ffffff;
  --surface-subtle: #fafafa;
  --border: #e6e6e6;
  --border-strong: #d4d4d4;
  --text: #1f2328;
  --muted: #6b7280;
  --folder: #dcb67a;
  --lean: #2563eb;
  --config: #64748b;
  --docs: #9ca3af;
  --bar-lemma: #7c3aed;
  --bar-theorem: #2563eb;
  --bar-def: #059669;
  --bar-structure: #ea580c;
  --bar-instance: #db2777;
  --bar-other: #94a3b8;
  --radius: 0px;
  --mono: "SFMono-Regular", Consolas, Monaco, "Liberation Mono", monospace;
}

* { box-sizing: border-box; }
html, body {
  margin: 0;
  height: 100%;
  overflow: hidden;
  background: var(--bg);
}
body {
  font-family: Inter, ui-sans-serif, system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  color: var(--text);
  font-size: 15px;
}

#app-shell {
  --left-panel-width: 380px;
  --right-panel-width: 400px;
  --paper-code-panel-width: var(--right-panel-width);
  height: 100vh;
  display: grid;
  grid-template-columns: var(--left-panel-width) 6px minmax(0, 1fr) 6px var(--right-panel-width);
  background: var(--bg);
  overflow: hidden;
}

#app-shell.paper-balanced-layout {
  grid-template-columns: var(--left-panel-width) 6px minmax(0, 1fr) 6px minmax(0, 1fr);
}

.panel-surface {
  min-height: 0;
  background: var(--surface);
  border-right: 1px solid var(--border);
}

.sidebar {
  --sidebar-top-fr: 50;
  min-height: 0;
  height: 100vh;
  display: grid;
  grid-template-rows: minmax(220px, calc(var(--sidebar-top-fr) * 1%)) 6px minmax(180px, 1fr);
  overflow: hidden;
}

.repo-panel,
.overview-panel,
.main-stage,
.semantic-panel {
  min-height: 0;
  display: grid;
  overflow: hidden;
}

.repo-panel {
  grid-template-rows: auto auto auto 1fr;
}

.overview-panel,
.semantic-panel {
  grid-template-rows: auto 1fr;
}

.overview-panel {
  border-top: 1px solid var(--border);
}

.main-stage {
  grid-template-rows: 1fr;
}

.semantic-panel {
  border-right: none;
}


.splitter {
  background: #f6f7f9;
  position: relative;
  z-index: 3;
}
.splitter::after {
  content: '';
  position: absolute;
  inset: 0;
}
.splitter-vertical {
  cursor: col-resize;
  border-left: 1px solid var(--border);
  border-right: 1px solid var(--border);
}
.splitter-horizontal {
  cursor: row-resize;
  border-top: 1px solid var(--border);
  border-bottom: 1px solid var(--border);
}
body.is-resizing-col { cursor: col-resize; }
body.is-resizing-row { cursor: row-resize; }

.panel-title-row {
  padding: 10px 14px;
  border-bottom: 1px solid var(--border);
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 8px;
}

.panel-title-row.compact h2 {
  margin: 0;
  font-size: 1rem;
  font-weight: 600;
}

.overview-panel .panel-title-row.compact {
  height: 36px;
  min-height: 36px;
  padding: 5px 10px;
  gap: 12px;
  background: #ffffff;
}

.overview-panel .panel-title-row.compact h2 {
  color: #111827;
  font-size: 0.86rem;
  font-weight: 760;
  line-height: 1;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}

.semantic-panel .panel-title-row.compact {
  height: 43px;
  min-height: 43px;
  padding: 0 14px;
}

.repo-panel .panel-title-row.compact {
  height: 43px;
  min-height: 43px;
  padding: 0 14px;
}

.repo-panel .panel-title-row.compact h2 {
  line-height: 1;
}

.panel-title-with-actions {
  display: flex;
  align-items: center;
  gap: 8px;
}

.toolbar-row {
  display: grid;
  grid-template-columns: minmax(120px, 150px) minmax(0, 1fr);
  gap: 8px;
  padding: 8px 12px;
  border-bottom: 1px solid var(--border);
  background: var(--surface-subtle);
}

.repo-panel .toolbar-row {
  height: 44px;
  min-height: 44px;
  padding: 6px 10px;
}

.toolbar-input,
.icon-button {
  border: 1px solid var(--border-strong);
  background: #fff;
  color: var(--text);
  font: inherit;
}

.toolbar-input {
  width: 100%;
  height: 34px;
  padding: 0 10px;
  font-size: 0.9rem;
  outline: none;
}

.toolbar-input:focus {
  border-color: #2563eb;
}

.inline-actions {
  display: flex;
  gap: 6px;
}

.icon-button {
  width: 30px;
  height: 30px;
  padding: 0;
  cursor: pointer;
  line-height: 1;
}

.icon-button:hover {
  background: #f6f8fa;
}

.ghost-button {
  width: 26px;
  height: 26px;
  border-color: transparent;
  color: var(--muted);
}

.repo-legend {
  display: grid;
  gap: 10px;
  padding: 10px 12px;
  border-bottom: 1px solid var(--border);
  background: #fffdf8;
}

.repo-legend.hidden {
  display: none;
}

.legend-row {
  display: flex;
  align-items: center;
  gap: 14px;
  flex-wrap: wrap;
}

.legend-item,
.legend-color-item {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  color: var(--muted);
  font-size: 0.8rem;
}

.legend-swatch {
  width: 10px;
  height: 10px;
  border-radius: 2px;
}

.tree-container,
.selection-overview,
.graph-stage,
.semantic-preview {
  min-height: 0;
  overflow: auto;
}

.semantic-preview.has-source-panel {
  overflow: hidden;
  padding: 0;
}

.tree-container {
  padding: 6px 0 10px;
}

.tree-item {
  display: grid;
}

.tree-row {
  padding: 0 8px;
  cursor: pointer;
  border-left: 2px solid transparent;
}

.tree-row:hover {
  background: #f6f8fa;
}

.tree-row.selected {
  background: #e8f0fe;
  border-left-color: #2563eb;
}

.tree-row.dimmed {
  opacity: 0.34;
}

.tree-row.dimmed:hover {
  opacity: 0.64;
}

.tree-line {
  min-height: 28px;
  display: grid;
  grid-template-columns: auto auto minmax(0, 1fr) auto auto;
  align-items: center;
  gap: 6px;
}

.tree-toggle,
.tree-indent {
  width: 14px;
  height: 14px;
  display: inline-flex;
  align-items: center;
  justify-content: center;
  color: var(--muted);
  font-size: 0.76rem;
  flex: 0 0 auto;
}

.tree-toggle {
  border: none;
  background: transparent;
  cursor: pointer;
  padding: 0;
}

.node-icon {
  width: 14px;
  height: 14px;
  display: inline-flex;
  align-items: center;
  justify-content: center;
  color: var(--docs);
}

.node-icon svg {
  width: 14px;
  height: 14px;
  display: block;
}

.node-icon.folder { color: var(--folder); }
.node-icon.lean { color: var(--lean); }
.node-icon.config { color: var(--config); }
.node-icon.docs,
.node-icon.other { color: var(--docs); }

.tree-name {
  font-size: 0.9rem;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
  line-height: 1.28;
}

.tree-inline-stats {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  color: var(--muted);
  font-size: 0.76rem;
  margin-left: 10px;
}

.compact-stat {
  white-space: nowrap;
}

.tree-row-detail {
  padding-left: 20px;
}

.tree-row-detail.folder-status {
  margin-top: -4px;
  padding-bottom: 3px;
}

.tree-row-detail.file-status {
  padding-top: 1px;
  padding-bottom: 5px;
}

.tree-bar {
  width: 100%;
  height: 5px;
  display: flex;
  overflow: hidden;
  background: #f1f5f9;
  border-radius: 999px;
}

.tree-bar span { height: 100%; }
.bar-lemma { background: var(--bar-lemma); }
.bar-theorem { background: var(--bar-theorem); }
.bar-def { background: var(--bar-def); }
.bar-structure { background: var(--bar-structure); }
.bar-instance { background: var(--bar-instance); }
.bar-other { background: var(--bar-other); }

.selection-overview {
  padding: 7px 10px;
  font-size: 0.92rem;
}

.selection-overview .paper-focus-block {
  margin-top: 0;
  padding-top: 0;
}

.selection-overview .paper-focus-block > .paper-match-card:first-child {
  padding-top: 2px;
}

.semantic-preview {
  padding: 12px 14px;
  font-size: 0.92rem;
}

.graph-stage {
  padding: 0;
  min-height: 0;
}

.overview-block,
.preview-block {
  display: grid;
  gap: 14px;
}

.overview-headline,
.placeholder-title {
  font-size: 0.95rem;
  font-weight: 600;
}

.path-line,
.code-line {
  font-family: var(--mono);
  font-size: 0.78rem;
  color: var(--muted);
  word-break: break-word;
}

.selection-meta,
.semantic-meta,
.metric-grid {
  display: flex;
  flex-wrap: wrap;
  gap: 8px;
}

.meta-chip {
  border: 1px solid var(--border);
  padding: 2px 6px;
  font-size: 0.74rem;
  color: var(--muted);
  background: #fff;
}

.overview-list,
.semantic-list,
.semantic-stack {
  display: grid;
  gap: 8px;
}

.overview-item,
.semantic-item {
  display: grid;
  gap: 4px;
  padding: 8px 0;
  border-top: 1px solid #f1f5f9;
}

.overview-item:first-child,
.semantic-item:first-child { border-top: none; }

.item-title {
  display: flex;
  align-items: flex-start;
  flex-wrap: wrap;
  justify-content: space-between;
  gap: 8px;
  font-size: 0.86rem;
}

.item-title strong {
  font-weight: 600;
  min-width: 0;
  overflow-wrap: anywhere;
}

.item-subtitle,
.section-help {
  color: var(--muted);
  font-size: 0.78rem;
}

.section-heading {
  font-size: 0.8rem;
  font-weight: 600;
  color: var(--muted);
  text-transform: uppercase;
  letter-spacing: 0.03em;
}

.focus-composition {
  display: grid;
  gap: 6px;
}

.focus-composition .tree-bar {
  height: 6px;
}

.main-placeholder {
  height: 100%;
  display: grid;
  place-items: center;
  text-align: center;
  color: var(--muted);
  padding: 22px;
}

.placeholder-inner {
  max-width: 520px;
  display: grid;
  gap: 12px;
}

.placeholder-metrics {
  display: flex;
  justify-content: center;
  flex-wrap: wrap;
  gap: 8px;
}

.placeholder-chip {
  border: 1px solid var(--border);
  padding: 4px 8px;
  font-size: 0.78rem;
  color: var(--text);
  background: #fff;
}

.empty-state {
  color: var(--muted);
  font-size: 0.86rem;
}

@media (max-width: 1260px) {
  #app-shell {
    grid-template-columns: minmax(280px, 360px) 6px minmax(0, 1fr);
  }

  #splitter-right,
  .semantic-panel {
    display: none;
  }
}

@media (max-width: 860px) {
  html, body {
    overflow: auto;
  }

  #app-shell {
    height: auto;
    min-height: 100vh;
    grid-template-columns: 1fr;
  }

  .splitter {
    display: none;
  }

  .sidebar {
    height: auto;
    min-height: auto;
    grid-template-rows: minmax(380px, 1fr) minmax(260px, auto);
  }

  .main-stage {
    min-height: 360px;
    border-top: 1px solid var(--border);
  }
}



.graph-shell {
  height: 100%;
  display: grid;
  grid-template-rows: auto auto 1fr;
  min-height: 0;
}

.graph-tabs {
  display: flex;
  gap: 6px;
  padding: 8px 12px 0;
  border-bottom: 1px solid var(--border);
  background: #fff;
  overflow-x: auto;
}

.graph-tab {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  height: 34px;
  padding: 0 12px;
  border: 1px solid var(--border);
  border-bottom: none;
  background: #fafafa;
  color: var(--muted);
  font: inherit;
  cursor: pointer;
  white-space: nowrap;
}

.graph-tab.active {
  background: #fff;
  color: var(--text);
  border-color: var(--border-strong);
  font-weight: 600;
}

.graph-tab-close {
  font-size: 1rem;
  color: #94a3b8;
}

.graph-toolbar {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 14px;
  padding: 10px 14px;
  border-bottom: 1px solid var(--border);
  background: #ffffff;
}

.graph-toolbar.graph-toolbar-compact {
  min-height: 44px;
  padding: 7px 10px;
  align-items: center;
  gap: 10px;
}

.graph-toolbar-compact .graph-toolbar-stack {
  gap: 2px;
  min-width: 0;
}

.graph-toolbar-compact .graph-toolbar-stack strong {
  font-size: 0.95rem;
  line-height: 1.08;
  font-weight: 650;
}

.graph-toolbar-compact .graph-meta-row {
  gap: 6px;
  min-height: 0;
  line-height: 1.15;
}

.graph-toolbar-compact .graph-chip {
  padding: 0;
  border: 0;
  background: transparent;
  font-size: 0.74rem;
  line-height: 1.15;
}

.graph-toolbar-compact .graph-toolbar-right {
  align-items: center;
  gap: 6px;
}

.graph-toolbar-compact .graph-control,
.graph-toolbar-compact .filter-chip.compact {
  font-size: 0.72rem;
}

.graph-toolbar-compact .toolbar-input.compact-select,
.graph-toolbar-compact .graph-mode-button,
.graph-toolbar-compact .graph-button {
  height: 24px;
  font-size: 0.72rem;
}

.graph-toolbar-stack {
  display: grid;
  gap: 8px;
}

.graph-mode-row,
.graph-meta-row {
  display: flex;
  align-items: center;
  gap: 8px;
  flex-wrap: wrap;
}

.graph-toolbar-right {
  display: flex;
  align-items: center;
  gap: 8px;
  flex-wrap: wrap;
  justify-content: flex-end;
}

.graph-study-controls {
  max-width: 420px;
}

.graph-control {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  font-size: 0.82rem;
  color: var(--muted);
}

.graph-control select { min-width: 62px; }

.graph-mode-button,
.graph-button {
  height: 30px;
  padding: 0 10px;
  border: 1px solid var(--border-strong);
  background: #fff;
  color: var(--text);
  font: inherit;
  cursor: pointer;
}

.graph-mode-button.active {
  border-color: #2563eb;
  color: #1d4ed8;
  background: #eff6ff;
}

.graph-mode-button:disabled {
  opacity: 0.45;
  cursor: default;
}

.graph-button:hover,
.graph-mode-button:hover:not(:disabled) {
  background: #f6f8fa;
}
.graph-chip {
  border: 1px solid var(--border);
  padding: 3px 8px;
  font-size: 0.82rem;
  color: var(--muted);
  background: #fff;
}

.graph-chip.muted {
  color: #8b949e;
}

.graph-legend-inline {
  gap: 6px;
  color: var(--muted);
  font-size: 0.8rem;
}

.legend-dot {
  width: 14px;
  height: 10px;
  display: inline-block;
  border: 2px solid #64748b;
  background: #f8fafc;
  border-radius: 999px;
}

.legend-dot.shape-rect {
  border-radius: 3px;
}

.legend-dot.shape-ellipse {
  border-radius: 999px;
}

.legend-dot.shape-round {
  border-radius: 7px;
}

.legend-dot.shape-diamond {
  width: 11px;
  height: 11px;
  margin-inline: 2px;
  border-radius: 2px;
  transform: rotate(45deg);
}

.legend-dot.shape-hex {
  border-radius: 0;
  clip-path: polygon(25% 0%, 75% 0%, 100% 50%, 75% 100%, 25% 100%, 0% 50%);
}

.legend-dot.shape-octagon {
  border-radius: 0;
  clip-path: polygon(32% 0%, 68% 0%, 100% 28%, 100% 72%, 68% 100%, 32% 100%, 0% 72%, 0% 28%);
}

.legend-dot.root-preview {
  border-color: #111827;
  background: rgba(15, 23, 42, 0.10);
  border-radius: 999px;
}

.legend-dot.context-preview {
  border-color: #64748b;
  background: rgba(100, 116, 139, 0.10);
  border-radius: 999px;
}

.legend-line {
  display: inline-block;
  width: 18px;
  height: 0;
  border-top: 2px solid #94a3b8;
}

.legend-line.strong {
  border-top-color: #475569;
}

.legend-line.dashed {
  border-top-style: dashed;
}

.legend-text {
  margin-right: 6px;
}

.graph-canvas {
  min-height: 0;
  position: relative;
  overflow: hidden;
  background: #ffffff;
}

.graph-svg {
  width: 100%;
  height: 100%;
  display: block;
  cursor: grab;
  user-select: none;
}

.graph-svg:active {
  cursor: grabbing;
}

.legend-badge {
  width: 12px;
  height: 12px;
  display: inline-block;
  border-radius: 999px;
  border: 1px solid #fff;
  box-shadow: 0 0 0 1px rgba(148, 163, 184, 0.35);
}

.legend-badge.entry {
  background: #f59e0b;
}

.legend-badge.terminal {
  background: #0f766e;
}

.legend-badge.incomplete {
  width: 12px;
  height: 12px;
  border-radius: 3px;
  background: #dc2626;
}

.graph-edge {
  stroke: #a8b0bb;
  stroke-width: 1.4;
  stroke-opacity: 0.65;
}

.graph-edge.backbone {
  stroke: #64748b;
  stroke-width: 1.8;
}

.graph-edge.dense {
  stroke-width: 0.7;
  stroke-opacity: 0.28;
}

.graph-edge.selected {
  stroke: #1d4ed8;
  stroke-width: 1.8;
  stroke-opacity: 0.95;
}

.graph-edge.muted,
.graph-edge.dim {
  stroke-opacity: 0.18;
  stroke-dasharray: 4 4;
}

.graph-edge.active {
  stroke: #0f172a;
  stroke-width: 2;
  stroke-opacity: 0.95;
}

.graph-edge.focus-tree {
  stroke: #0891b2;
  stroke-width: 2.35;
  stroke-opacity: 0.98;
  stroke-dasharray: none;
}

.graph-node-group {
  cursor: pointer;
}

.graph-node-group.dim,
.graph-node-group.muted {
  opacity: 0.22;
}

.graph-node-shape {
  stroke: #ffffff;
  stroke-width: 1.6;
}

.graph-node-shape.dense {
  stroke-width: 0.6;
}

.graph-node-shape.highlighted {
  stroke: #1d4ed8;
  stroke-width: 2.2;
}

.graph-node-shape.focus {
  stroke: #0f172a;
  stroke-width: 2.6;
}

.graph-node-shape.root {
  stroke: #111827;
  stroke-width: 3;
}

.graph-node-shape.selected-node {
  stroke: #2563eb;
  stroke-width: 2.6;
}

.graph-node-shape.terminal {
  filter: drop-shadow(0 1px 0 rgba(0,0,0,0.08));
}

.graph-label {
  fill: #334155;
  font-size: 12px;
  pointer-events: none;
}

.graph-label.inside {
  fill: #0f172a;
  font-size: 14px;
  font-weight: 650;
}

.graph-label.inside.paper-node-label {
  font-size: 14px;
  font-weight: 750;
  letter-spacing: -0.01em;
}

.graph-label.focus {
  fill: #0f172a;
  font-weight: 700;
}

.graph-label.root {
  text-decoration: underline;
}
.semantic-detail {
  gap: 12px;
}

.semantic-header {
  display: grid;
  gap: 8px;
}

.semantic-title-row {
  display: flex;
  align-items: center;
  gap: 8px;
  flex-wrap: wrap;
}

.meta-chip.accent {
  color: #1d4ed8;
  border-color: #bfdbfe;
  background: #eff6ff;
}

.code-block {
  margin: 0;
  white-space: pre-wrap;
  word-break: break-word;
  border: 1px solid var(--border);
  background: #fafafa;
  padding: 10px;
  font-size: 0.8rem;
  line-height: 1.45;
  font-family: var(--mono);
  color: #111827;
}

.code-block.secondary {
  background: #f8fafc;
}

.semantic-paragraph {
  color: var(--text);
  font-size: 0.86rem;
  line-height: 1.5;
}

.neighbor-list {
  display: grid;
  gap: 6px;
}

.neighbor-item {
  display: flex;
  justify-content: space-between;
  gap: 8px;
  align-items: center;
  width: 100%;
  padding: 7px 9px;
  border: 1px solid var(--border);
  background: #fff;
  color: var(--text);
  text-align: left;
  cursor: pointer;
  font: inherit;
}

.neighbor-item:hover,
.overview-item:hover {
  background: #f8fafc;
}

.neighbor-main {
  font-weight: 600;
  font-size: 0.84rem;
}

.neighbor-meta {
  color: var(--muted);
  font-size: 0.76rem;
}

.overview-item {
  cursor: pointer;
}


.selection-preview {
  border-color: #2563eb;
  background: rgba(37, 99, 235, 0.10);
}

.touchpoint-preview {
  border-color: #d97706;
  background: rgba(217, 119, 6, 0.12);
}

.focus-tree-preview {
  border-color: #0891b2;
  background: rgba(8, 145, 178, 0.14);
}

.incomplete-preview {
  border-color: #dc2626;
  background: rgba(220, 38, 38, 0.12);
}

.graph-edge.contextual {
  stroke: #94a3b8;
  stroke-width: 1.45;
  stroke-opacity: 0.72;
  stroke-dasharray: 4 4;
}

.graph-node-shape.selection-hit {
  stroke: #2563eb;
  stroke-width: 2.4;
}

.graph-node-shape.touchpoint {
  stroke: #d97706;
  stroke-width: 2.2;
  stroke-dasharray: 5 3;
}

.graph-node-shape.focus-tree {
  stroke: #0891b2;
  stroke-width: 2.25;
  filter: drop-shadow(0 1px 2px rgba(8, 145, 178, 0.20));
}

.graph-node-shape.contextual {
  opacity: 0.95;
  stroke: #64748b;
  stroke-width: 1.8;
}

.graph-node-shape.incomplete {
  stroke: #dc2626;
  stroke-dasharray: 5 3;
}

.meta-chip.warning {
  color: #b91c1c;
  border-color: #fecaca;
  background: #fef2f2;
}

.filter-row {
  display: flex;
  gap: 8px;
  padding: 8px 12px;
  border-bottom: 1px solid var(--border);
  background: #fff;
  flex-wrap: wrap;
}

.filter-chip {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  font-size: 0.84rem;
  color: var(--muted);
  border: 1px solid var(--border);
  padding: 4px 8px;
  background: #fafafa;
}

.filter-chip input { margin: 0; }
.filter-chip.disabled { opacity: 0.45; }

.toolbar-button {
  border: 1px solid var(--border-strong);
  background: #fff;
  color: var(--text);
  font: inherit;
  height: 32px;
  padding: 0 10px;
  cursor: pointer;
  white-space: nowrap;
}
.toolbar-button:hover:not(:disabled) { background: #f6f8fa; }
.toolbar-button:disabled {
  opacity: 0.42;
  background: transparent;
  color: var(--muted);
  cursor: not-allowed;
}
.toolbar-button.accent { border-color: #c7d7ff; background: #eef4ff; }

.section-actions {
  display: flex;
  gap: 8px;
  flex-wrap: wrap;
  margin-top: 10px;
}

.metric-grid.two-col {
  grid-template-columns: repeat(2, minmax(0, 1fr));
}

.meta-chip.warning {
  border-color: #f2c37d;
  background: #fff7eb;
  color: #9a5b00;
}

.meta-chip.accent {
  border-color: #c7d7ff;
  background: #eef4ff;
  color: #1849a9;
}

.semantic-item .section-heading {
  font-weight: 600;
  margin-bottom: 8px;
}

.semantic-list,
.overview-list,
.neighbor-list {
  display: grid;
  gap: 8px;
}

.overview-item,
.neighbor-item,
.path-step {
  border: 1px solid var(--border);
  background: #fff;
  padding: 10px;
}

.overview-item.clickable,
.neighbor-item,
.path-step.clickable {
  cursor: pointer;
}
.overview-item.clickable:hover,
.neighbor-item:hover,
.path-step.clickable:hover { background: #f9fbff; }

.item-title,
.path-step-head {
  display: flex;
  align-items: flex-start;
  flex-wrap: wrap;
  justify-content: space-between;
  gap: 8px;
}

.item-subtitle,
.path-step-reason {
  margin-top: 4px;
  color: var(--muted);
  font-size: 0.88rem;
  line-height: 1.35;
}

.path-step-index {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  width: 20px;
  height: 20px;
  border-radius: 50%;
  background: #eef4ff;
  color: #1849a9;
  font-size: 0.76rem;
  font-weight: 700;
}

.semantic-header {
  display: grid;
  gap: 10px;
  margin-bottom: 4px;
}

.semantic-title-row {
  display: flex;
  align-items: center;
  gap: 8px;
  flex-wrap: wrap;
}

.placeholder-title {
  font-size: 1.05rem;
  font-weight: 650;
}

.semantic-paragraph {
  line-height: 1.45;
  color: var(--text);
}

.code-block {
  margin: 0;
  padding: 10px;
  border: 1px solid var(--border);
  background: #fafafa;
  overflow: auto;
  white-space: pre-wrap;
  font-family: var(--mono);
  font-size: 0.82rem;
  line-height: 1.45;
}

.code-block.secondary {
  margin-top: 8px;
  background: #fcfcfc;
}

.file-open-anchor {
  color: #1849a9;
  text-decoration: underline;
  cursor: pointer;
}

.tree-row-actions {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  margin-left: auto;
  white-space: nowrap;
}

.file-modal {
  position: fixed;
  inset: 0;
  z-index: 40;
  overflow: hidden;
  padding: 24px;
}
.file-modal.hidden { display: none; }
.file-modal-backdrop {
  position: fixed;
  inset: 0;
  background: rgba(15, 23, 42, 0.24);
}
.file-modal-dialog {
  position: relative;
  background: #fff;
  border: 1px solid var(--border-strong);
  display: grid;
  grid-template-rows: auto 1fr;
  height: calc(100vh - 48px);
}
.file-modal-header {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 16px;
  padding: 14px 16px;
  border-bottom: 1px solid var(--border);
}
.file-modal-title-wrap h2 {
  margin: 2px 0 0;
  font-size: 1.1rem;
}
.file-modal-subtitle {
  margin-top: 4px;
  color: var(--muted);
  font-size: 0.9rem;
  overflow-wrap: anywhere;
}
.file-modal-actions {
  display: flex;
  gap: 8px;
}
.file-modal-body {
  min-height: 0;
  display: grid;
  grid-template-columns: clamp(400px, 34vw, 520px) minmax(0, 1fr);
}
.file-modal-sidebar {
  min-height: 0;
  overflow: hidden;
  border-right: 1px solid var(--border);
  padding: 12px;
  display: grid;
  grid-template-rows: auto minmax(0, 1fr);
  gap: 12px;
  background: #fbfbfb;
}
.file-modal-meta {
  display: grid;
  gap: 12px;
  align-content: start;
}
.file-modal-outline {
  min-height: 0;
  display: grid;
  grid-template-rows: auto minmax(0, 1fr);
  gap: 12px;
  overflow: hidden;
}
.file-outline-list {
  min-height: 0;
  overflow: auto;
  align-content: start;
  padding-right: 4px;
}
.file-modal-editor-wrap {
  min-height: 0;
  display: grid;
  grid-template-rows: auto 1fr;
  overflow: hidden;
}
.file-modal-status {
  padding: 8px 12px;
  border-bottom: 1px solid var(--border);
  color: var(--muted);
  font-size: 0.88rem;
}
.file-modal-editor {
  min-height: 0;
  overflow: auto;
  background: #ffffff;
  font-family: var(--mono);
  font-size: 0.84rem;
  line-height: 1.45;
}
.file-editor-table {
  width: 100%;
  border-collapse: collapse;
}
.file-editor-table td {
  vertical-align: top;
}
.file-line-number {
  width: 56px;
  padding: 0 10px 0 12px;
  color: #9ca3af;
  text-align: right;
  user-select: none;
  border-right: 1px solid #f1f3f5;
}
.file-line-code {
  white-space: pre;
  padding: 0 12px;
}
.file-line {
  border-left: 3px solid transparent;
}
.file-line.color-kind-lemma { background: rgba(124, 58, 237, 0.05); }
.file-line.color-kind-theorem { background: rgba(37, 99, 235, 0.05); }
.file-line.color-kind-def { background: rgba(5, 150, 105, 0.05); }
.file-line.color-kind-structure { background: rgba(234, 88, 12, 0.05); }
.file-line.color-kind-instance { background: rgba(219, 39, 119, 0.05); }
.file-line.color-kind-other { background: rgba(148, 163, 184, 0.05); }
.file-line.color-status-proved { background: rgba(22, 163, 74, 0.06); }
.file-line.color-status-incomplete { background: rgba(220, 38, 38, 0.05); }
.file-line.focused {
  background: rgba(15, 23, 42, 0.08) !important;
  border-left-color: #334155;
}
.file-line.decl-start .file-line-number { color: #64748b; font-weight: 700; }
.file-outline-item {
  border: 1px solid var(--border);
  border-left: 4px solid transparent;
  padding: 8px 10px;
  background: #fff;
  cursor: pointer;
}
.file-outline-item:hover { background: #f8fbff; }
.file-outline-item.active { border-color: #b7cdfd; background: #eef4ff; }
.file-outline-item.color-kind-lemma { border-left-color: var(--bar-lemma); }
.file-outline-item.color-kind-theorem { border-left-color: var(--bar-theorem); }
.file-outline-item.color-kind-def { border-left-color: var(--bar-def); }
.file-outline-item.color-kind-structure { border-left-color: var(--bar-structure); }
.file-outline-item.color-kind-instance { border-left-color: var(--bar-instance); }
.file-outline-item.color-kind-other { border-left-color: var(--bar-other); }
.file-outline-item.color-status-proved { border-left-color: #16a34a; }
.file-outline-item.color-status-incomplete { border-left-color: #dc2626; }
.file-outline-title { font-weight: 600; }
.file-outline-title,
.file-outline-meta {
  overflow-wrap: anywhere;
}
.file-outline-meta { color: var(--muted); font-size: 0.84rem; margin-top: 4px; }
.file-meta-group {
  border: 1px solid var(--border);
  background: #fff;
  padding: 10px;
  display: grid;
  gap: 8px;
}
.file-meta-group .section-heading { margin: 0; }
.file-meta-group .metric-grid.two-col {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
}
.file-meta-group .meta-chip {
  min-width: 0;
  overflow-wrap: anywhere;
}

.file-color-mode {
  display: flex;
  justify-content: flex-start;
}
.file-color-label {
  display: inline-flex;
  align-items: center;
  flex-wrap: wrap;
  gap: 8px;
  font-size: 0.84rem;
  color: var(--muted);
  min-width: 0;
  max-width: 100%;
}
.compact-select {
  height: 30px;
  min-width: 120px;
  max-width: 100%;
}

.file-color-legend {
  display: grid;
  gap: 6px;
  min-width: 0;
}
.file-color-legend-title {
  color: var(--muted);
  font-size: 0.78rem;
  font-weight: 600;
}
.file-color-legend-row {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
  min-width: 0;
}
@media (max-width: 1180px) {
  .file-modal-body {
    grid-template-columns: 1fr;
    grid-template-rows: auto minmax(0, 1fr);
  }

  .file-modal-sidebar {
    max-height: min(46vh, 520px);
    border-right: 0;
    border-bottom: 1px solid var(--border);
  }
}
.file-color-chip {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  border: 1px solid var(--border);
  background: #fff;
  padding: 4px 8px;
  border-radius: 999px;
  font-size: 0.78rem;
  color: var(--text);
  min-width: 0;
  max-width: 100%;
}
.file-color-swatch {
  width: 10px;
  height: 10px;
  border-radius: 999px;
  border: 1px solid rgba(15, 23, 42, 0.08);
  background: currentColor;
}
.file-color-chip.color-kind-lemma { color: var(--bar-lemma); }
.file-color-chip.color-kind-theorem { color: var(--bar-theorem); }
.file-color-chip.color-kind-def { color: var(--bar-def); }
.file-color-chip.color-kind-structure { color: var(--bar-structure); }
.file-color-chip.color-kind-instance { color: var(--bar-instance); }
.file-color-chip.color-kind-other { color: var(--bar-other); }
.file-color-chip.color-status-proved { color: #16a34a; }
.file-color-chip.color-status-incomplete { color: #dc2626; }
.focus-card {
  border-radius: 4px;
  padding: 6px 8px;
}
.section-actions.compact {
  margin-top: 8px;
}

.file-source-missing {
  padding: 18px;
  color: var(--muted);
}

/* graph polish iteration */
.graph-toolbar {
  align-items: center;
}
.graph-toolbar-stack {
  min-width: 0;
}
.graph-meta-row {
  row-gap: 6px;
}
.graph-toolbar-right {
  flex-shrink: 0;
}
.graph-canvas-actions {
  position: absolute;
  top: 12px;
  right: 12px;
  display: flex;
  gap: 8px;
  z-index: 4;
}
.graph-icon-button {
  width: 34px;
  height: 34px;
  border-radius: 999px;
  border: 1px solid rgba(15, 23, 42, 0.10);
  background: rgba(255,255,255,0.94);
  box-shadow: 0 2px 10px rgba(15,23,42,0.08);
  color: #334155;
  cursor: pointer;
  font: inherit;
}
.graph-icon-button:hover:not(:disabled) {
  background: #ffffff;
  border-color: rgba(37,99,235,0.22);
  color: #1d4ed8;
}
.graph-icon-button:disabled {
  opacity: 0.42;
  cursor: default;
}
.graph-legend-overlay {
  position: absolute;
  inset: 0;
  z-index: 6;
}
.graph-legend-backdrop {
  position: absolute;
  inset: 0;
  background: rgba(15, 23, 42, 0.24);
}
.graph-legend-modal {
  position: absolute;
  left: 50%;
  top: 50%;
  transform: translate(-50%, -50%);
  width: min(860px, calc(100% - 48px));
  max-height: calc(100% - 48px);
  overflow: auto;
  background: #fff;
  border: 1px solid var(--border);
  box-shadow: 0 16px 40px rgba(15,23,42,0.16);
  padding: 16px 18px;
}
.graph-legend-modal-header {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 12px;
  margin-bottom: 12px;
}
.graph-legend-subtitle {
  margin-top: 4px;
  color: var(--muted);
  font-size: 0.86rem;
}
.graph-legend-sections {
  display: grid;
  gap: 14px;
}
.graph-legend-section {
  border-top: 1px solid var(--border);
  padding-top: 12px;
}
.graph-legend-section:first-child {
  border-top: none;
  padding-top: 0;
}
.graph-legend-title {
  font-size: 0.92rem;
  font-weight: 600;
  margin-bottom: 8px;
}
.graph-legend-grid {
  display: flex;
  flex-wrap: wrap;
  gap: 8px 14px;
}
.graph-legend-help {
  color: var(--muted);
  font-size: 0.88rem;
  line-height: 1.45;
}
.paper-legend-reading-grid {
  display: grid;
  grid-template-columns: repeat(2, minmax(240px, 1fr));
  gap: 10px 14px;
}
.paper-legend-reading-item {
  display: grid;
  grid-template-columns: 52px minmax(0, 1fr);
  gap: 10px;
  align-items: center;
  padding: 9px;
  border: 1px solid var(--border);
  background: #f8fafc;
}
.paper-legend-reading-item strong {
  display: block;
  color: #111827;
  font-size: 0.82rem;
}
.paper-legend-reading-item span:not(.paper-legend-reading-sample) {
  display: block;
  margin-top: 1px;
  color: #475569;
  font-size: 0.74rem;
  font-weight: 700;
  text-transform: uppercase;
  letter-spacing: 0.035em;
}
.paper-legend-reading-item p {
  margin: 4px 0 0;
  color: var(--muted);
  font-size: 0.78rem;
  line-height: 1.34;
}
.paper-legend-reading-sample {
  position: relative;
  display: inline-block;
  width: 42px;
  height: 28px;
  border: 3px solid #15803d;
  background: #dcfce7;
}
.paper-legend-reading-sample span {
  position: absolute;
  top: -8px;
  right: -9px;
  display: inline-grid;
  place-items: center;
  width: 18px;
  height: 18px;
  border-radius: 999px;
  border: 1.5px solid #ffffff;
  background: #15803d;
  color: #ffffff;
  font-size: 7px;
  font-weight: 850;
  line-height: 1;
  box-shadow: 0 0 0 1px rgba(15, 23, 42, 0.16);
}
.paper-legend-reading-status {
  border-color: #15803d;
  background: #dcfce7;
}
.paper-legend-reading-status span {
  background: #15803d;
}
.paper-legend-reading-badge {
  border-color: #64748b;
  background: #f8fafc;
}
.paper-legend-reading-badge span {
  background: #dc2626;
}
.paper-status-legend-item {
  gap: 8px;
}
.paper-legend-status-node {
  position: relative;
  display: inline-block;
  width: 30px;
  height: 18px;
  border: 3px solid #64748b;
  background: #f8fafc;
}
.paper-legend-status-node span {
  position: absolute;
  top: -8px;
  right: -9px;
  display: inline-grid;
  place-items: center;
  min-width: 16px;
  height: 16px;
  padding: 0 3px;
  border-radius: 999px;
  border: 1.5px solid #ffffff;
  background: #64748b;
  color: #ffffff;
  font-size: 8px;
  font-weight: 850;
  line-height: 1;
  box-shadow: 0 0 0 1px rgba(15, 23, 42, 0.16);
}
.paper-legend-status-node.paper-formalization-formalized { border-color: #15803d; }
.paper-legend-status-node.paper-formalization-formalized { background: #dcfce7; }
.paper-legend-status-node.paper-formalization-formalized span { background: #15803d; }
.paper-legend-status-node.paper-formalization-statement_only { border-color: #65a30d; }
.paper-legend-status-node.paper-formalization-statement_only { background: #ecfccb; }
.paper-legend-status-node.paper-formalization-statement_only span { background: #65a30d; }
.paper-legend-status-node.paper-formalization-partial { border-color: #d97706; }
.paper-legend-status-node.paper-formalization-partial { background: #fef3c7; }
.paper-legend-status-node.paper-formalization-partial span { background: #d97706; }
.paper-legend-status-node.paper-formalization-blueprint_only { border-color: #2563eb; }
.paper-legend-status-node.paper-formalization-blueprint_only { background: #dbeafe; }
.paper-legend-status-node.paper-formalization-blueprint_only span { background: #2563eb; font-size: 7px; }
.paper-legend-status-node.paper-formalization-not_locally_formalized { border-color: #dc2626; }
.paper-legend-status-node.paper-formalization-not_locally_formalized { background: #fee2e2; }
.paper-legend-status-node.paper-formalization-not_locally_formalized span { background: #dc2626; }
@media (max-width: 760px) {
  .paper-legend-reading-grid {
    grid-template-columns: 1fr;
  }
}
.legend-line.active {
  border-top-color: #0f172a;
}
.selected-preview {
  border-color: #0f172a;
  background: rgba(15, 23, 42, 0.12);
}
.terminal-preview {
  border-color: #0f766e;
  background: rgba(15, 118, 110, 0.12);
}
.entry-preview {
  border-color: #f59e0b;
  background: rgba(245, 158, 11, 0.16);
}
.graph-node-group {
  transition: opacity 120ms ease;
}
.graph-node-shape,
.graph-label,
.graph-edge {
  transition: stroke 140ms ease, stroke-opacity 140ms ease, opacity 140ms ease, fill 140ms ease;
}
.graph-node-shape.root {
  stroke: #111827;
  stroke-width: 3.3;
}
.graph-node-shape.selected-node,
.graph-node-shape.focus {
  stroke: #2563eb;
  stroke-width: 3;
}
.graph-node-shape.focus.root {
  stroke: #111827;
}
.graph-edge {
  stroke-linecap: round;
}

/* Compound declaration nodes used by study graphs. */
.graph-node-shape.compound-node {
  stroke: none;
}

.compound-outer {
  fill: #ffffff;
  stroke: #cbd5e1;
  stroke-width: 1.1;
  filter: drop-shadow(0 1px 3px rgba(15, 23, 42, 0.10));
}

.graph-node-shape.compound-node.focus .compound-outer,
.graph-node-shape.compound-node.selected-node .compound-outer {
  stroke: #2563eb;
  stroke-width: 2.1;
}

.graph-node-shape.compound-node.root .compound-outer {
  stroke: #111827;
  stroke-width: 2.1;
}

.graph-node-shape.compound-node.incomplete .compound-outer {
  stroke-dasharray: 5 3;
}

.compound-header {
  opacity: 0.95;
}

.compound-separator {
  stroke: #e5e7eb;
  stroke-width: 1;
}

.compound-title {
  fill: #ffffff;
  font-size: 11px;
  font-weight: 650;
  pointer-events: none;
}

.compound-layer-label {
  font-size: 9px;
  font-weight: 700;
  letter-spacing: 0.04em;
  text-transform: uppercase;
  pointer-events: none;
}

.compound-layer-label.signature {
  fill: #1d4ed8;
}

.compound-layer-label.proof {
  fill: #c2410c;
}

.compound-signature-text {
  fill: #334155;
  font-family: var(--mono);
  font-size: 10.2px;
  pointer-events: none;
}

.compound-proof-text {
  fill: #7c2d12;
  font-family: var(--mono);
  font-size: 9.4px;
  pointer-events: none;
}

.graph-edge.type-ref {
  stroke: #2563eb;
  stroke-opacity: 0.78;
}

.graph-edge.value-ref {
  stroke: #ea580c;
  stroke-opacity: 0.72;
}

.graph-edge.type-ref.active {
  stroke: #2563eb;
  stroke-width: 2.2;
  stroke-opacity: 0.95;
}

.graph-edge.value-ref.active {
  stroke: #ea580c;
  stroke-width: 2.2;
  stroke-opacity: 0.95;
}

.graph-edge.type-ref.dim,
.graph-edge.value-ref.dim {
  stroke-opacity: 0.18;
}

.legend-line.type-ref {
  border-top-color: #2563eb;
}

.legend-line.value-ref {
  border-top-color: #ea580c;
}

/* Inline source reader used in the right panel. It replaces the old popup workflow. */
.source-panel {
  min-height: 100%;
  height: 100%;
  display: grid;
  grid-template-rows: auto minmax(0, 1fr);
  min-width: 0;
  overflow: hidden;
  background: #fff;
}
.source-panel.source-panel-code-only {
  grid-template-rows: minmax(0, 1fr);
}
.source-panel-summary {
  display: grid;
  gap: 4px;
  padding: 4px 6px;
  border-bottom: 1px solid var(--border);
  background: #fbfbfb;
  min-width: 0;
}
.source-file-name {
  font-size: 0.92rem;
  font-weight: 650;
  line-height: 1.2;
  color: var(--text);
  margin: 0;
  min-width: 0;
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
  padding-left: 14px;
  text-indent: -14px;
}
.semantic-paragraph.compact {
  margin: 0;
  font-size: 0.88rem;
}
.source-summary-text {
  line-height: 1.55;
  min-width: 0;
  overflow-wrap: anywhere;
  word-break: break-word;
}
.source-summary-token {
  font-weight: 600;
}
.source-summary-token.color-kind-lemma {
  color: var(--bar-lemma);
}
.source-summary-token.color-kind-theorem {
  color: var(--bar-theorem);
}
.source-summary-token.color-kind-def {
  color: var(--bar-def);
}
.source-summary-token.color-kind-structure {
  color: var(--bar-structure);
}
.source-summary-token.color-kind-instance {
  color: var(--bar-instance);
}
.source-summary-token.color-kind-other {
  color: var(--bar-other);
}
.source-summary-token.color-status-proved {
  color: #16a34a;
}
.source-summary-token.color-status-incomplete {
  color: #dc2626;
}
.source-color-mode {
  margin-top: 0;
  min-width: 0;
}
.source-panel-body {
  min-height: 0;
  display: grid;
  grid-template-columns: minmax(0, 1fr);
  overflow: hidden;
}
.source-outline {
  min-height: 0;
  display: grid;
  grid-template-rows: auto minmax(0, 1fr);
  gap: 10px;
  overflow: hidden;
  padding: 10px;
  border-right: 1px solid var(--border);
  background: #fbfbfb;
}
.source-editor-wrap {
  min-height: 0;
  display: grid;
  grid-template-rows: minmax(0, 1fr);
  overflow: hidden;
}
.source-editor-shell {
  position: relative;
  min-height: 0;
  overflow: hidden;
}
.source-editor {
  min-height: 0;
  height: 100%;
  font-size: 0.8rem;
  padding-right: 16px;
  scrollbar-width: none;
  -ms-overflow-style: none;
}
.source-editor::-webkit-scrollbar {
  width: 0;
  height: 0;
}
.source-minimap {
  position: absolute;
  top: 0;
  right: 0;
  bottom: 0;
  width: 14px;
  z-index: 2;
  background: linear-gradient(180deg, rgba(250, 250, 250, 0.96) 0%, rgba(243, 244, 246, 0.96) 100%);
  border-left: 1px solid rgba(230, 230, 230, 0.85);
  overflow: hidden;
}
.source-minimap-track {
  position: absolute;
  inset: 6px 2px;
  border-radius: 999px;
  background: rgba(148, 163, 184, 0.12);
  overflow: hidden;
}
.source-minimap-segment {
  position: absolute;
  left: 0;
  right: 0;
  z-index: 1;
  border: 0;
  padding: 0;
  margin: 0;
  cursor: pointer;
  opacity: 0.72;
}
.source-minimap-segment:hover {
  opacity: 0.95;
}
.source-minimap-segment.active {
  box-shadow: inset 0 0 0 1px rgba(15, 23, 42, 0.22);
  opacity: 1;
}
.source-minimap-viewport {
  position: absolute;
  left: 0;
  right: 0;
  top: 0;
  z-index: 2;
  min-height: 18px;
  border: 1px solid rgba(15, 23, 42, 0.45);
  background: rgba(255, 255, 255, 0.18);
  box-shadow: inset 0 0 0 1px rgba(255, 255, 255, 0.4);
  pointer-events: none;
}
.source-minimap-segment.color-kind-lemma { background: rgba(124, 58, 237, 0.78); }
.source-minimap-segment.color-kind-theorem { background: rgba(37, 99, 235, 0.78); }
.source-minimap-segment.color-kind-def { background: rgba(5, 150, 105, 0.78); }
.source-minimap-segment.color-kind-structure { background: rgba(234, 88, 12, 0.78); }
.source-minimap-segment.color-kind-instance { background: rgba(219, 39, 119, 0.78); }
.source-minimap-segment.color-kind-other { background: rgba(148, 163, 184, 0.88); }
.source-minimap-segment.color-status-proved { background: rgba(22, 163, 74, 0.78); }
.source-minimap-segment.color-status-incomplete { background: rgba(220, 38, 38, 0.82); }
.source-editor-table .file-line {
  cursor: default;
}
.source-editor-table {
  table-layout: fixed;
}
.source-editor-table .source-graph-action-col {
  width: 18px;
}
.source-editor-table .source-line-number-col {
  width: 34px;
}
.source-editor-table .file-line-number {
  width: auto;
  padding: 0 4px 0 1px;
  text-align: left;
}
.source-line-number-text {
  display: block;
}
.file-line-graph-action {
  position: relative;
  padding: 0;
  vertical-align: stretch;
}
.source-editor-table .file-line-code {
  white-space: pre-wrap;
  overflow-wrap: anywhere;
  word-break: break-word;
}
.source-editor-table .file-line[data-decl-id] {
  cursor: pointer;
}
.source-editor-table .file-line[data-decl-id]:hover .file-line-code {
  background: transparent;
}
.source-editor-table .file-line {
  --source-rgb: 148, 163, 184;
}
.source-editor-table .file-line.color-kind-lemma { --source-rgb: 124, 58, 237; }
.source-editor-table .file-line.color-kind-theorem { --source-rgb: 37, 99, 235; }
.source-editor-table .file-line.color-kind-def { --source-rgb: 5, 150, 105; }
.source-editor-table .file-line.color-kind-structure { --source-rgb: 234, 88, 12; }
.source-editor-table .file-line.color-kind-instance { --source-rgb: 219, 39, 119; }
.source-editor-table .file-line.color-kind-other { --source-rgb: 148, 163, 184; }
.source-editor-table .file-line.color-status-proved { --source-rgb: 22, 163, 74; }
.source-editor-table .file-line.color-status-incomplete { --source-rgb: 220, 38, 38; }
.source-editor-table .file-line[data-decl-id]:hover {
  background: rgba(var(--source-rgb), 0.12);
}
.source-editor-table .file-line.decl-statement {
  background: rgba(var(--source-rgb), 0.10);
}
.source-editor-table .file-line.decl-statement .file-line-code {
  font-weight: 400;
}
.source-editor-table .file-line.decl-proof {
  background: rgba(var(--source-rgb), 0.045);
}
.source-editor-table .file-line.decl-proof .file-line-number {
  color: #9ca3af;
}
.source-editor-table .file-line.decl-proof-start .file-line-code {
  box-shadow: inset 0 1px 0 rgba(var(--source-rgb), 0.18);
}
.file-line.color-kind-lemma { border-left-color: rgba(124, 58, 237, 0.7); }
.file-line.color-kind-theorem { border-left-color: rgba(37, 99, 235, 0.7); }
.file-line.color-kind-def { border-left-color: rgba(5, 150, 105, 0.7); }
.file-line.color-kind-structure { border-left-color: rgba(234, 88, 12, 0.7); }
.file-line.color-kind-instance { border-left-color: rgba(219, 39, 119, 0.7); }
.file-line.color-kind-other { border-left-color: rgba(148, 163, 184, 0.7); }
.source-editor-table .file-line.focused.focus-signature {
  background: rgba(var(--source-rgb), 0.16) !important;
  border-left-color: rgba(var(--source-rgb), 0.95) !important;
  font-weight: 600;
}
.source-editor-table .file-line.focused.focus-signature .file-line-code {
  font-weight: 600;
}
.source-editor-table .file-line.focused.focus-proof {
  background: rgba(var(--source-rgb), 0.075) !important;
  border-left-color: rgba(var(--source-rgb), 0.82) !important;
}
.inline-code-action {
  position: absolute;
  inset: 2px 0 2px 1px;
  width: auto;
  min-height: 20px;
  display: inline-flex;
  align-items: center;
  justify-content: center;
  border: 1px solid #1d4ed8;
  border-radius: 4px;
  background: #2563eb;
  color: #fff;
  padding: 0;
  cursor: pointer;
  box-shadow: inset 0 1px 0 rgba(255, 255, 255, 0.24), 0 0 0 1px rgba(37, 99, 235, 0.1);
}
.inline-code-action svg {
  width: 14px;
  height: 14px;
  display: block;
}
.inline-code-action:hover {
  background: #1d4ed8;
  border-color: #1e40af;
  color: #fff;
}
.inline-code-action:focus-visible {
  outline: 2px solid #2563eb;
  outline-offset: 1px;
}
.source-panel .focus-card {
  margin: 0;
}
.source-panel .file-color-legend-row {
  gap: 4px;
}
.source-panel .file-color-chip {
  font-size: 0.76rem;
}

@media (max-width: 1280px) {
  .source-panel-body {
    grid-template-columns: 1fr;
    grid-template-rows: minmax(150px, 30%) minmax(0, 1fr);
  }
  .source-outline {
    border-right: 0;
    border-bottom: 1px solid var(--border);
  }
}

/* Node border encodes code status. Fill encodes proof state. */
.graph-node-shape.proved-code:not(.compound-node) {
  stroke: #087f36 !important;
  stroke-width: 2.8;
  stroke-dasharray: none;
}
.graph-node-shape.lean-incomplete:not(.compound-node),
.graph-node-shape.incomplete:not(.compound-node) {
  stroke: #2563eb !important;
  stroke-width: 3;
  stroke-dasharray: 5 3;
}
.graph-node-shape.external-lean:not(.compound-node) {
  stroke: #facc15 !important;
  stroke-width: 3.2;
  stroke-dasharray: 7 4;
}
.graph-node-shape.no-lean-code:not(.compound-node) {
  stroke: #dc2626 !important;
  stroke-width: 3.2;
  stroke-dasharray: 7 4;
}
.graph-node-shape.proved-code.focus:not(.compound-node),
.graph-node-shape.proved-code.selected-node:not(.compound-node) {
  stroke: #087f36 !important;
  stroke-width: 3.6;
}
.graph-node-shape.lean-incomplete.focus:not(.compound-node),
.graph-node-shape.lean-incomplete.selected-node:not(.compound-node),
.graph-node-shape.incomplete.focus:not(.compound-node),
.graph-node-shape.incomplete.selected-node:not(.compound-node) {
  stroke: #1d4ed8 !important;
  stroke-width: 3.8;
  stroke-dasharray: 5 3;
}
.graph-node-shape.external-lean.focus:not(.compound-node),
.graph-node-shape.external-lean.selected-node:not(.compound-node) {
  stroke: #facc15 !important;
  stroke-width: 3.8;
  stroke-dasharray: 7 4;
}
.graph-node-shape.no-lean-code.focus:not(.compound-node),
.graph-node-shape.no-lean-code.selected-node:not(.compound-node) {
  stroke: #b91c1c !important;
  stroke-width: 3.8;
  stroke-dasharray: 7 4;
}
.legend-dot.external-lean-preview {
  border-color: #facc15;
  border-style: dashed;
  background: #ffffff;
}
.legend-dot.no-lean-preview {
  border-color: #dc2626;
  border-style: dashed;
  background: #ffffff;
  border-radius: 999px;
}
.legend-dot.incomplete-code-preview {
  border-color: #2563eb;
  background: #ffffff;
  border-radius: 999px;
}
.legend-dot.proved-code-preview {
  border-color: #087f36;
  background: #ffffff;
  border-radius: 999px;
}

.graph-edge.graphviz-spline {
  stroke-opacity: 0.52;
  stroke-width: 1.15;
}

.graph-edge.graphviz-spline.dim {
  stroke-opacity: 0.08;
  stroke-dasharray: none;
}

.graph-edge.graphviz-spline.focus-tree,
.graph-edge.graphviz-spline.active,
.graph-edge.graphviz-spline.selected {
  stroke: #0f172a;
  stroke-opacity: 0.92;
  stroke-width: 2.1;
}


/* Compact blueprint overview overrides */
.graph-edge {
  stroke: #111827;
  stroke-width: 1.65;
  stroke-opacity: 0.78;
  stroke-linecap: round;
  stroke-linejoin: round;
}

.graph-edge.backbone,
.graph-edge.contextual,
.graph-edge.graphviz-spline,
.graph-edge.type-ref,
.graph-edge.value-ref {
  stroke: #111827;
  stroke-width: 1.65;
  stroke-opacity: 0.78;
}

.graph-edge.selected,
.graph-edge.active,
.graph-edge.focus-tree,
.graph-edge.graphviz-spline.focus-tree,
.graph-edge.graphviz-spline.active,
.graph-edge.graphviz-spline.selected,
.graph-edge.type-ref.active,
.graph-edge.value-ref.active {
  stroke: #000000;
  stroke-width: 2.35;
  stroke-opacity: 0.98;
}

.graph-edge.dim,
.graph-edge.muted,
.graph-edge.graphviz-spline.dim,
.graph-edge.type-ref.dim,
.graph-edge.value-ref.dim {
  opacity: 0.16;
  stroke-opacity: 0.78;
  stroke-dasharray: none;
}

.graph-label.inside {
  font-size: 17px;
  font-weight: 400;
  letter-spacing: -0.015em;
}

.graph-label.focus,
.graph-label.root {
  font-weight: 400;
}

/* Readable labels with medium compact spacing */
.graph-label.inside {
  font-size: 22px;
  font-weight: 400;
  letter-spacing: -0.02em;
}

.graph-label.focus,
.graph-label.root {
  font-weight: 400;
}

/* Blueprint-faithful Graphviz sizing: use Graphviz node geometry as source of truth. */
.graph-label.inside {
  font-size: 14px;
  font-weight: 400;
  letter-spacing: 0;
}

.graph-label.focus,
.graph-label.root {
  font-weight: 400;
}

.graph-edge,
.graph-edge.backbone,
.graph-edge.contextual,
.graph-edge.graphviz-spline,
.graph-edge.type-ref,
.graph-edge.value-ref {
  stroke: #111827;
  stroke-width: 1.15;
  stroke-opacity: 0.82;
  stroke-linecap: round;
  stroke-linejoin: round;
}

.graph-edge.selected,
.graph-edge.active,
.graph-edge.focus-tree,
.graph-edge.graphviz-spline.focus-tree,
.graph-edge.graphviz-spline.active,
.graph-edge.graphviz-spline.selected {
  stroke: #000000;
  stroke-width: 1.8;
  stroke-opacity: 0.96;
}

.graph-edge.dim,
.graph-edge.muted,
.graph-edge.graphviz-spline.dim {
  opacity: 0.18;
  stroke-opacity: 0.82;
  stroke-dasharray: none;
}

/* Synchronized with DOT fontsize=22. Graphviz computes node size with this font. */
.graph-label.inside {
  font-size: 22px;
  font-weight: 400;
}

/* Full labels, synchronized with DOT fontsize=22. */
.graph-label.inside {
  font-size: 22px;
  font-weight: 400;
}
.graph-label.focus,
.graph-label.root {
  font-weight: 400;
}

/* File dependency map. */
.graph-chip.accent {
  border-color: #93c5fd;
  color: #1d4ed8;
  background: #eff6ff;
}

.graph-folders {
  pointer-events: none;
}

.file-folder-box {
  fill: rgba(248, 250, 252, 0.78);
  stroke: #cbd5e1;
  stroke-width: 1.1;
  stroke-dasharray: 6 5;
}

.file-folder-group.depth-1 .file-folder-box,
.file-folder-group.depth-2 .file-folder-box {
  fill: rgba(241, 245, 249, 0.70);
}

.file-folder-label {
  fill: #475569;
  font-size: 12px;
  font-weight: 700;
  pointer-events: none;
}

.file-folder-summary {
  fill: #94a3b8;
  font-size: 10px;
  font-weight: 600;
  pointer-events: none;
}

.graph-node-shape.file-node-shape {
  stroke: #ffffff;
  stroke-width: 1.8;
  filter: drop-shadow(0 1px 3px rgba(15, 23, 42, 0.12));
}

.graph-node-shape.file-node-shape.proved-code {
  stroke: #087f36 !important;
  stroke-width: 2.8;
  stroke-dasharray: none;
}

.graph-node-shape.file-node-shape.lean-incomplete,
.graph-node-shape.file-node-shape.incomplete {
  stroke: #2563eb !important;
  stroke-width: 3;
  stroke-dasharray: 5 3;
}

.graph-node-shape.file-node-shape.file-status-empty {
  fill: #f1f5f9;
  stroke: #cbd5e1 !important;
  stroke-width: 1.8;
  stroke-dasharray: 4 4;
}

.graph-node-shape.file-node-shape.focus,
.graph-node-shape.file-node-shape.selected-node,
.graph-node-shape.file-node-shape.focus-tree {
  stroke: #0f172a !important;
  stroke-width: 3.4;
  stroke-dasharray: none;
}

.graph-label.file-title {
  fill: #0f172a;
  font-size: 12.5px;
  font-weight: 400;
  pointer-events: none;
}

.graph-label.file-title.focus {
  fill: #0f172a;
}

.graph-label.file-summary {
  fill: #334155;
  font-size: 11.25px;
  font-weight: 400;
  pointer-events: none;
}

.graph-label.file-summary.warning {
  fill: #1d4ed8;
}

.graph-label.file-deps {
  fill: #64748b;
  font-size: 9.5px;
  font-weight: 600;
  pointer-events: none;
}

.empty-file-preview {
  border-color: #cbd5e1;
  border-style: dashed;
  background: #f1f5f9;
}

/* Project map swimlane layout. Folders organize space; file nodes carry status. */
.file-folder-box {
  fill: #f8fafc;
  stroke: #d6dee8;
  stroke-width: 1.1;
  stroke-dasharray: none;
  rx: 12;
}

.file-folder-group:nth-child(even) .file-folder-box {
  fill: #f4f7fb;
}

.file-folder-label {
  fill: #334155;
  font-size: 13px;
  font-weight: 760;
  letter-spacing: -0.01em;
}

.file-folder-summary {
  fill: #94a3b8;
  font-size: 10.5px;
  font-weight: 650;
}

.graph-edge.file-import-edge,
.graph-edge.file-import-edge.backbone,
.graph-edge.file-import-edge.contextual {
  stroke: #64748b;
  stroke-width: 1.05;
  stroke-opacity: 0.32;
  fill: none;
  stroke-linecap: round;
  stroke-linejoin: round;
}

.graph-edge.file-import-edge.active,
.graph-edge.file-import-edge.file-focus-edge,
.graph-edge.file-import-edge.selected {
  stroke: #0f172a;
  stroke-width: 1.9;
  stroke-opacity: 0.92;
}

.graph-edge.file-import-edge.dim,
.graph-edge.file-import-edge.file-nonfocus-edge {
  opacity: 0.08;
  stroke-dasharray: none;
}

.graph-node-shape.file-node-shape {
  filter: drop-shadow(0 1px 2px rgba(15, 23, 42, 0.12));
}

.graph-label.file-title {
  font-size: 12.5px;
  font-weight: 400;
}

.graph-label.file-summary {
  font-size: 11.25px;
  font-weight: 400;
}

/* Hierarchical Project map. Expanded folders are containers; collapsed folders are nodes. */
.filter-chip.button-like {
  cursor: pointer;
  font-family: inherit;
}

.graph-folders {
  pointer-events: visiblePainted;
}

.file-folder-group .file-folder-box {
  fill: rgba(248, 250, 252, 0.62);
  stroke: #cbd5e1;
  stroke-width: 1.1;
  stroke-dasharray: 7 5;
}

.file-folder-group.depth-1 .file-folder-box,
.file-folder-group.root-folder .file-folder-box {
  fill: rgba(241, 245, 249, 0.74);
  stroke: #94a3b8;
  stroke-width: 1.35;
}

.file-folder-group.depth-2 .file-folder-box {
  fill: rgba(248, 250, 252, 0.72);
  stroke: #cbd5e1;
}

.file-folder-label.clickable {
  cursor: pointer;
  pointer-events: auto;
  user-select: none;
}
.file-folder-label.clickable:hover {
  fill: #0f172a;
  text-decoration: underline;
}

.graph-node-shape.folder-node-shape {
  fill: #ffffff;
  stroke: #94a3b8;
  stroke-width: 1.6;
  stroke-dasharray: 7 4;
  filter: drop-shadow(0 1px 2px rgba(15, 23, 42, 0.10));
}
.graph-node-shape.folder-node-shape.contains-incomplete {
  stroke: #2563eb;
  stroke-width: 2.1;
}
.graph-node-shape.folder-node-shape.focus,
.graph-node-shape.folder-node-shape.focus-tree,
.graph-node-shape.folder-node-shape.selection-hit {
  stroke: #0f172a;
  stroke-width: 2.6;
  stroke-dasharray: none;
}
.graph-label.folder-title {
  fill: #0f172a;
  font-weight: 790;
}
.graph-label.folder-summary {
  fill: #475569;
}
.graph-label.folder-hint {
  fill: #94a3b8;
  font-size: 9px;
}

/* Project map focus interactions. */
.file-selected-halo {
  fill: none;
  stroke: #0f172a;
  stroke-width: 4.5;
  stroke-opacity: 0.24;
  pointer-events: none;
}

.graph-node-group.dim {
  opacity: 0.12;
}

.graph-node-shape.file-node-shape.focus,
.graph-node-shape.file-node-shape.selected-node {
  stroke: #0f172a !important;
  stroke-width: 5.2 !important;
  stroke-dasharray: none !important;
  filter: drop-shadow(0 6px 12px rgba(15, 23, 42, 0.28));
}

.graph-edge.file-import-edge.folder-selection-edge,
.graph-edge.file-import-edge.file-focus-edge {
  stroke: #0f172a;
  stroke-width: 2.2;
  stroke-opacity: 0.95;
}

.graph-edge.file-import-edge.file-nonfocus-edge {
  opacity: 0.055;
}

/* Project map edges follow the blueprint visual language.
   Selection emphasizes the dependency closure but keeps the full DAG visible. */
.graph-edge.file-import-edge,
.graph-edge.file-import-edge.backbone,
.graph-edge.file-import-edge.contextual,
.graph-edge.file-import-edge.graphviz-spline {
  stroke: #334155 !important;
  stroke-width: 1.05 !important;
  stroke-opacity: 0.42 !important;
  opacity: 1 !important;
  stroke-linecap: round;
  stroke-linejoin: round;
  stroke-dasharray: none !important;
  fill: none;
}

.graph-edge.file-import-edge.active,
.graph-edge.file-import-edge.file-focus-edge,
.graph-edge.file-import-edge.folder-selection-edge,
.graph-edge.file-import-edge.selected,
.graph-edge.file-import-edge.graphviz-spline.active,
.graph-edge.file-import-edge.graphviz-spline.selected {
  stroke: #000000 !important;
  stroke-width: 1.8 !important;
  stroke-opacity: 0.96 !important;
  opacity: 1 !important;
  stroke-dasharray: none !important;
}

.graph-edge.file-import-edge.dim,
.graph-edge.file-import-edge.file-nonfocus-edge,
.graph-edge.file-import-edge.graphviz-spline.dim {
  stroke: #334155 !important;
  stroke-width: 1.05 !important;
  stroke-opacity: 0.34 !important;
  opacity: 0.16 !important;
  stroke-dasharray: none !important;
}

.graph-node-group.dim {
  opacity: 0.28 !important;
}

.graph-node-shape.file-node-shape {
  filter: none;
}

.graph-node-shape.file-node-shape.focus,
.graph-node-shape.file-node-shape.selected-node {
  stroke: #0f172a !important;
  stroke-width: 4.2 !important;
  stroke-dasharray: none !important;
  filter: drop-shadow(0 4px 8px rgba(15, 23, 42, 0.20));
}

.file-selected-halo {
  stroke: #0f172a !important;
  stroke-width: 4 !important;
  stroke-opacity: 0.20 !important;
}

/* Declaration-projected focus on the Project map. */
.graph-label.file-decl-projection {
  font-size: 15px;
  font-weight: 450;
  pointer-events: none;
}

.graph-label.file-decl-projection.selected-decl {
  fill: #0f172a;
}

.graph-label.file-decl-projection.related-decl {
  fill: #1d4ed8;
}

.graph-label.file-title.decl-projection-primary {
  fill: #020617;
  font-weight: 500;
}

.graph-label.file-summary.with-decl-projection {
  font-size: 17px;
}

.file-selected-halo.decl-projection-halo {
  stroke: #2563eb !important;
  stroke-width: 5 !important;
  stroke-opacity: 0.28 !important;
}

.graph-node-shape.file-node-shape.focus-tree {
  stroke: #1d4ed8 !important;
  stroke-width: 2.6 !important;
}

.graph-node-shape.file-node-shape.focus,
.graph-node-shape.file-node-shape.selected-node {
  stroke: #0f172a !important;
  stroke-width: 4.2 !important;
}

.source-decl-info-row td {
  border: 0;
}

.source-decl-info-cell {
  padding: 8px 10px 8px 6px;
  background: #ffffff;
}

.inline-decl-card {
  border: 1px solid rgba(15, 23, 42, 0.14);
  border-left: 4px solid #2563eb;
  border-radius: 10px;
  background: linear-gradient(180deg, #ffffff, #f8fafc);
  box-shadow: 0 8px 24px rgba(15, 23, 42, 0.08);
  padding: 10px 12px;
  display: grid;
  gap: 8px;
}

.source-decl-info-row.color-kind-lemma .inline-decl-card { border-left-color: rgb(109, 40, 217); }
.source-decl-info-row.color-kind-theorem .inline-decl-card { border-left-color: rgb(29, 78, 216); }
.source-decl-info-row.color-kind-def .inline-decl-card { border-left-color: rgb(4, 120, 87); }
.source-decl-info-row.color-kind-structure .inline-decl-card { border-left-color: rgb(194, 65, 12); }
.source-decl-info-row.color-kind-instance .inline-decl-card { border-left-color: rgb(190, 24, 93); }
.source-decl-info-row.color-status-incomplete .inline-decl-card { border-left-color: rgb(185, 28, 28); }

.inline-decl-card-main {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 12px;
}

.inline-decl-card-title {
  display: flex;
  align-items: center;
  gap: 7px;
  min-width: 0;
  color: #0f172a;
}

.inline-decl-card-title strong {
  font-size: 13px;
  line-height: 1.25;
  overflow-wrap: anywhere;
}

.inline-decl-kind,
.inline-decl-status,
.inline-decl-chip {
  display: inline-flex;
  align-items: center;
  border-radius: 999px;
  border: 1px solid rgba(148, 163, 184, 0.34);
  background: #f8fafc;
  color: #334155;
  font-size: 11px;
  line-height: 1;
  padding: 4px 7px;
  white-space: nowrap;
}

.inline-decl-kind {
  color: #1d4ed8;
  background: rgba(37, 99, 235, 0.08);
  border-color: rgba(37, 99, 235, 0.18);
  font-weight: 700;
}

.inline-decl-status.proved {
  color: #166534;
  background: rgba(22, 163, 74, 0.09);
  border-color: rgba(22, 163, 74, 0.24);
}

.inline-decl-status.incomplete {
  color: #991b1b;
  background: rgba(220, 38, 38, 0.08);
  border-color: rgba(220, 38, 38, 0.22);
}

.inline-decl-card-subtitle {
  margin-top: 5px;
  color: #64748b;
  font-size: 11px;
}

.inline-decl-card-action {
  border: 1px solid rgba(37, 99, 235, 0.22);
  border-radius: 8px;
  background: rgba(37, 99, 235, 0.08);
  color: #1d4ed8;
  font-weight: 650;
  font-size: 11px;
  padding: 5px 8px;
  cursor: pointer;
  flex: 0 0 auto;
}

.inline-decl-card-action:hover {
  background: rgba(37, 99, 235, 0.13);
  border-color: rgba(37, 99, 235, 0.34);
}

.inline-decl-metrics {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
}

.inline-decl-chip {
  border-radius: 8px;
  line-height: 1.25;
  white-space: normal;
}

.inline-decl-chip.active {
  color: #1e3a8a;
  background: rgba(37, 99, 235, 0.08);
  border-color: rgba(37, 99, 235, 0.24);
}

.inline-decl-chip.local-only {
  color: #475569;
  background: rgba(100, 116, 139, 0.08);
  border-color: rgba(100, 116, 139, 0.18);
}

.inline-decl-chip.empty {
  color: #94a3b8;
  background: #f8fafc;
}

.inline-decl-hint {
  color: #64748b;
  font-size: 11px;
  line-height: 1.35;
}

/* Compact inline declaration dependency card. */
.source-decl-info-row.compact td {
  border: 0;
}

.source-decl-info-cell.compact {
  padding: 3px 8px 4px 6px;
  background: #ffffff;
}

.inline-decl-card.compact {
  display: inline-flex;
  align-items: center;
  flex-wrap: wrap;
  gap: 4px;
  width: auto;
  max-width: 100%;
  border: 1px solid rgba(148, 163, 184, 0.26);
  border-left: 3px solid #2563eb;
  border-radius: 7px;
  background: #ffffff;
  box-shadow: none;
  padding: 4px 6px;
}

.inline-decl-card.compact .inline-decl-card-label {
  color: #475569;
  font-size: 10px;
  font-weight: 750;
  letter-spacing: 0.02em;
  text-transform: uppercase;
  margin-right: 2px;
  white-space: nowrap;
}

.inline-decl-card.compact .inline-decl-chip {
  border-radius: 999px;
  font-size: 10.5px;
  line-height: 1;
  padding: 3px 6px;
  white-space: nowrap;
}

/* Distinguish Lean import vs public import in the Project map. */
.legend-line.public-import-preview {
  width: 34px;
  height: 0;
  border-top: 3px solid #111827;
  border-radius: 999px;
}

.graph-edge.file-import-edge.public-import-edge,
.graph-edge.file-import-edge.public-import-edge.backbone,
.graph-edge.file-import-edge.public-import-edge.contextual,
.graph-edge.file-import-edge.public-import-edge.graphviz-spline {
  stroke-width: 2.15 !important;
  stroke-opacity: 0.9 !important;
}

.graph-edge.file-import-edge.public-import-edge.active,
.graph-edge.file-import-edge.public-import-edge.file-focus-edge,
.graph-edge.file-import-edge.public-import-edge.folder-selection-edge,
.graph-edge.file-import-edge.public-import-edge.selected,
.graph-edge.file-import-edge.public-import-edge.graphviz-spline.active,
.graph-edge.file-import-edge.public-import-edge.graphviz-spline.selected {
  stroke-width: 2.8 !important;
  stroke-opacity: 1 !important;
}

.graph-edge.file-import-edge.private-import-edge {
  stroke-width: 1.1 !important;
}

/* Unified cross-view focus, public/private import colors, compact dependency card. */
.legend-line.strong {
  border-top-color: #475569 !important;
}
.legend-line.public-import-preview {
  width: 34px;
  height: 0;
  border-top: 3px solid #d97706 !important;
  border-radius: 999px;
}

.graph-edge.file-import-edge.private-import-edge,
.graph-edge.file-import-edge.private-import-edge.backbone,
.graph-edge.file-import-edge.private-import-edge.contextual,
.graph-edge.file-import-edge.private-import-edge.graphviz-spline {
  stroke: #475569 !important;
  stroke-width: 1.15 !important;
  stroke-opacity: 0.80 !important;
}

.graph-edge.file-import-edge.public-import-edge,
.graph-edge.file-import-edge.public-import-edge.backbone,
.graph-edge.file-import-edge.public-import-edge.contextual,
.graph-edge.file-import-edge.public-import-edge.graphviz-spline {
  stroke: #d97706 !important;
  stroke-width: 2.15 !important;
  stroke-opacity: 0.92 !important;
}

.graph-edge.file-import-edge.private-import-edge.active,
.graph-edge.file-import-edge.private-import-edge.file-focus-edge,
.graph-edge.file-import-edge.private-import-edge.folder-selection-edge,
.graph-edge.file-import-edge.private-import-edge.selected,
.graph-edge.file-import-edge.private-import-edge.graphviz-spline.active,
.graph-edge.file-import-edge.private-import-edge.graphviz-spline.selected {
  stroke: #0f172a !important;
  stroke-width: 1.9 !important;
  stroke-opacity: 0.97 !important;
}

.graph-edge.file-import-edge.public-import-edge.active,
.graph-edge.file-import-edge.public-import-edge.file-focus-edge,
.graph-edge.file-import-edge.public-import-edge.folder-selection-edge,
.graph-edge.file-import-edge.public-import-edge.selected,
.graph-edge.file-import-edge.public-import-edge.graphviz-spline.active,
.graph-edge.file-import-edge.public-import-edge.graphviz-spline.selected {
  stroke: #c2410c !important;
  stroke-width: 2.85 !important;
  stroke-opacity: 1 !important;
}

.graph-edge.file-import-edge.dim,
.graph-edge.file-import-edge.file-nonfocus-edge,
.graph-edge.file-import-edge.graphviz-spline.dim {
  opacity: 0.25 !important;
}

/* Related nodes keep their semantic/status border; only the selected node gets the strong black outline. */
.graph-node-shape.focus-tree:not(.selected-node):not(.focus) {
  stroke-width: inherit;
  filter: none;
}
.graph-node-shape.file-node-shape.file-status-complete.focus-tree:not(.selected-node):not(.focus) {
  stroke: #166534 !important;
  stroke-width: 1.7 !important;
  stroke-dasharray: none !important;
}
.graph-node-shape.file-node-shape.file-status-partial.focus-tree:not(.selected-node):not(.focus),
.graph-node-shape.file-node-shape.lean-incomplete.focus-tree:not(.selected-node):not(.focus),
.graph-node-shape.file-node-shape.incomplete.focus-tree:not(.selected-node):not(.focus) {
  stroke: #2563eb !important;
  stroke-width: 2.6 !important;
  stroke-dasharray: 5 3 !important;
}
.graph-node-shape.file-node-shape.file-status-empty.focus-tree:not(.selected-node):not(.focus) {
  stroke: #cbd5e1 !important;
  stroke-width: 1.8 !important;
  stroke-dasharray: 4 4 !important;
}
.graph-node-shape.focus,
.graph-node-shape.selected-node,
.graph-node-shape.file-node-shape.focus,
.graph-node-shape.file-node-shape.selected-node {
  stroke: #0f172a !important;
  stroke-width: 4.2 !important;
  stroke-dasharray: none !important;
  filter: drop-shadow(0 4px 8px rgba(15, 23, 42, 0.18));
}
.node-selected-halo,
.file-selected-halo {
  fill: none;
  stroke: #0f172a !important;
  stroke-width: 4 !important;
  stroke-opacity: 0.18 !important;
  pointer-events: none;
}
.node-selected-halo {
  rx: 10;
}
.file-selected-halo.decl-projection-halo {
  stroke: #0f172a !important;
  stroke-opacity: 0.22 !important;
}

.source-decl-info-row td,
.source-decl-info-cell {
  border: 0 !important;
  padding: 0 !important;
}
.source-decl-info-cell {
  white-space: normal !important;
}
.inline-decl-card.dependency-only {
  width: 100%;
  box-sizing: border-box;
  border-radius: 0 !important;
  border: 0;
  border-top: 1px solid rgba(148, 163, 184, 0.38);
  border-bottom: 1px solid rgba(148, 163, 184, 0.38);
  background: #f8fafc;
  box-shadow: none !important;
  padding: 5px 8px;
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 8px;
  min-height: 28px;
}
.inline-decl-card.dependency-only .inline-decl-deps {
  display: flex;
  align-items: center;
  gap: 6px;
  min-width: 0;
  overflow: hidden;
}
.inline-decl-card.dependency-only .inline-decl-chip {
  border-radius: 2px !important;
  padding: 3px 6px !important;
  font-size: 10px !important;
  line-height: 1.05 !important;
  max-width: 220px;
  overflow: hidden;
  text-overflow: ellipsis;
}
.inline-decl-graph-button {
  flex: 0 0 auto;
  width: auto !important;
  min-width: 78px !important;
  height: 22px !important;
  border-radius: 0 !important;
  margin-left: auto;
  padding: 0 9px !important;
  font-size: 10.5px !important;
  font-weight: 650 !important;
  letter-spacing: 0.01em;
  color: #0f172a !important;
  background: #ffffff !important;
  border: 1px solid rgba(15, 23, 42, 0.2) !important;
  white-space: nowrap;
}
.inline-decl-graph-button:hover {
  background: #e2e8f0 !important;
  border-color: rgba(15, 23, 42, 0.38) !important;
}
.file-line-graph-action:not(.has-action) {
  width: 6px;
  min-width: 6px;
}

.graph-node-shape.focus-tree:not(.selected-node):not(.focus):not(.file-node-shape) {
  stroke: #334155 !important;
  stroke-width: 1.35 !important;
  filter: none !important;
}
.graph-node-shape.proved-code.focus-tree:not(.selected-node):not(.focus):not(.file-node-shape) {
  stroke: #087f36 !important;
}
.graph-node-shape.lean-incomplete.focus-tree:not(.selected-node):not(.focus):not(.file-node-shape),
.graph-node-shape.incomplete.focus-tree:not(.selected-node):not(.focus):not(.file-node-shape) {
  stroke: #2563eb !important;
  stroke-width: 2.2 !important;
  stroke-dasharray: 5 3 !important;
}
.graph-node-shape.no-lean-code.focus-tree:not(.selected-node):not(.focus):not(.file-node-shape) {
  stroke: #ef4444 !important;
  stroke-width: 2.2 !important;
  stroke-dasharray: 5 3 !important;
}

/* Keep the Open graph button inside the selected-declaration dependency bar. */
.inline-decl-card.dependency-only .inline-decl-graph-button {
  position: static !important;
  inset: auto !important;
  display: inline-flex !important;
  align-items: center !important;
  justify-content: center !important;
  align-self: center !important;
  flex: 0 0 auto !important;
  margin-left: auto !important;
}

.inline-decl-card.dependency-only .inline-decl-graph-button + .inline-decl-graph-button {
  margin-left: 4px !important;
}

.inline-decl-card.dependency-only .inline-decl-blueprint-button {
  min-width: 100px !important;
  color: #1d4ed8 !important;
  border-color: rgba(37, 99, 235, 0.34) !important;
  background: #eff6ff !important;
}

.inline-decl-card.dependency-only .inline-decl-blueprint-button:hover {
  color: #1e40af !important;
  border-color: rgba(37, 99, 235, 0.52) !important;
  background: #dbeafe !important;
}

.inline-decl-card.dependency-only .inline-decl-deps {
  flex: 1 1 auto !important;
}


/* Experimental: Project map rendered with Blueprint graph sizing/configuration. */
.graph-node-shape.file-node-shape {
  rx: 7px;
  ry: 7px;
  stroke: rgba(15, 23, 42, 0.24);
  stroke-width: 2.1px;
  stroke-linejoin: round;
  filter: drop-shadow(0 1.5px 2.5px rgba(15, 23, 42, 0.14));
}

.graph-node-shape.file-node-shape.proved-code:not(.focus):not(.selected-node),
.graph-node-shape.file-node-shape.file-status-complete:not(.focus):not(.selected-node) {
  stroke: #0f7a3d !important;
  stroke-width: 2.15px !important;
}

.graph-label.file-title {
  font-size: 27px;
  font-weight: 640;
  letter-spacing: 0;
  text-rendering: geometricPrecision;
}

.graph-label.file-summary {
  font-size: 18.5px;
  font-weight: 520;
  letter-spacing: 0;
  text-rendering: geometricPrecision;
}

.graph-label.file-title.focus,
.graph-label.file-title.decl-projection-primary,
.graph-label.file-summary.with-decl-projection {
  font-weight: 560;
}

.graph-edge.file-import-edge,
.graph-edge.file-import-edge.backbone,
.graph-edge.file-import-edge.contextual,
.graph-edge.file-import-edge.graphviz-spline {
  stroke-width: 1.0;
}

/* Optional folder map overlay for Project map.
   Inspired by Graphviz gvmap: the layout remains unchanged; folders are drawn
   as soft map-like regions over the existing file positions. */
.folder-depth-control.is-disabled {
  opacity: 0.48;
}
.graph-folders {
  pointer-events: none;
}
.file-folder-region {
  pointer-events: none;
}
.file-folder-region-shape {
  fill: rgba(219, 234, 254, 0.12);
  stroke: rgba(37, 99, 235, 0.72);
  stroke-width: 2;
  stroke-linejoin: round;
  vector-effect: non-scaling-stroke;
  filter: drop-shadow(0 8px 14px rgba(15, 23, 42, 0.04));
}
.file-folder-region.depth-1 .file-folder-region-shape {
  fill: rgba(224, 231, 255, 0.11);
  stroke: rgba(79, 70, 229, 0.76);
  stroke-width: 2.35;
}
.file-folder-region.depth-2 .file-folder-region-shape {
  fill: rgba(219, 234, 254, 0.12);
  stroke: rgba(37, 99, 235, 0.72);
}
.file-folder-region.depth-3 .file-folder-region-shape {
  fill: rgba(204, 251, 241, 0.11);
  stroke: rgba(13, 148, 136, 0.74);
}
.file-folder-region.contains-incomplete .file-folder-region-shape {
  stroke-dasharray: 8 5;
}
.file-folder-region-label {
  fill: #1e293b;
  font-size: 12px;
  font-weight: 760;
  paint-order: stroke;
  stroke: rgba(255, 255, 255, 0.84);
  stroke-width: 3px;
  stroke-linejoin: round;
}
.file-folder-region-summary {
  fill: #64748b;
  font-size: 10px;
  font-weight: 650;
  paint-order: stroke;
  stroke: rgba(255, 255, 255, 0.84);
  stroke-width: 3px;
  stroke-linejoin: round;
}

.graph-label.file-area {
  fill: #64748b;
  font-size: 14px;
  font-weight: 600;
  pointer-events: none;
}

.area-legend-grid {
  grid-template-columns: repeat(auto-fit, minmax(170px, 1fr));
}

.graph-shell.has-project-overview {
  grid-template-rows: auto auto minmax(300px, 1.35fr) minmax(300px, 0.95fr);
}

.project-overview-panel {
  min-height: 0;
  overflow: auto;
  border-top: 1px solid var(--border);
  background: var(--surface);
  padding: 12px 14px 16px;
}

.project-overview-header {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 16px;
  padding-bottom: 8px;
  border-bottom: 1px solid var(--border);
  margin-bottom: 10px;
}

.project-overview-header h3 {
  margin: 2px 0 0;
  font-size: 1rem;
  font-weight: 600;
}

.eyebrow {
  color: var(--muted);
  font-size: 0.74rem;
  text-transform: uppercase;
  letter-spacing: 0.06em;
  font-weight: 700;
}


.project-overview-intro {
  display: block;
  margin-bottom: 16px;
}

.project-overview-narrative,
.project-overview-metrics,
.area-mini-graph-card,
.area-card-list {
  background: transparent;
  border: 0;
  border-radius: 0;
  box-shadow: none;
}

.project-overview-narrative {
  padding: 0;
  max-width: 1080px;
}

.overview-label {
  color: var(--muted);
  font-size: 0.74rem;
  font-weight: 700;
  text-transform: uppercase;
  letter-spacing: 0.04em;
  margin-bottom: 6px;
}

.project-overview-narrative p {
  margin: 0 0 8px;
  line-height: 1.42;
}

.project-overview-narrative p:last-child {
  margin-bottom: 0;
}

.overview-goal {
  font-size: 0.95rem;
  color: var(--text);
}

.math-inline,
.math-fn {
  font-family: ui-serif, Georgia, Cambria, "Times New Roman", Times, serif;
}

.overview-block {
  margin: 10px 0;
}

.overview-block-title {
  color: var(--muted);
  font-size: 0.72rem;
  font-weight: 700;
  text-transform: uppercase;
  letter-spacing: 0.04em;
  margin-bottom: 4px;
}

.overview-block ul {
  margin: 0;
  padding-left: 18px;
  display: grid;
  gap: 3px;
}

.overview-block li {
  line-height: 1.34;
}

.overview-term-list {
  display: flex;
  flex-wrap: wrap;
  gap: 5px;
}

.overview-term-list span {
  border: 1px solid var(--border);
  background: var(--surface-subtle);
  color: #475569;
  padding: 2px 6px;
  font-size: 0.74rem;
}

.overview-decl-table {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(220px, 1fr));
  gap: 3px 10px;
  max-width: 920px;
}

.overview-decl-row {
  display: flex;
  align-items: baseline;
  gap: 7px;
  min-width: 0;
  border-left: 2px solid #cbd5e1;
  padding-left: 7px;
  line-height: 1.25;
}

.overview-decl-row code {
  color: #0f172a;
  font-size: 0.76rem;
  white-space: nowrap;
}

.overview-decl-row span {
  color: #64748b;
  font-size: 0.70rem;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.project-overview-panel .mathjax-inline {
  display: none;
  font-family: ui-serif, Georgia, Cambria, "Times New Roman", Times, serif;
  white-space: nowrap;
}

.project-overview-panel.mathjax-ready .mathjax-inline {
  display: inline;
}

.project-overview-panel .math-fallback {
  display: inline;
  font-family: ui-serif, Georgia, Cambria, "Times New Roman", Times, serif;
  white-space: nowrap;
}

.project-overview-panel.mathjax-ready .math-fallback {
  display: none;
}

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

.reading-hint {
  color: #334155;
  font-weight: 600;
}

.project-overview-error {
  color: #92400e;
  background: #fffaf0;
  border: 1px solid #e7d39a;
  padding: 7px 8px;
}

.project-overview-metrics {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
  margin-top: 10px;
}

.project-overview-metric {
  display: inline-flex;
  align-items: baseline;
  gap: 5px;
  border: 1px solid var(--border);
  padding: 4px 7px;
  background: #fff;
}

.project-overview-metric strong {
  display: inline;
  font-size: 0.88rem;
  font-weight: 650;
}

.project-overview-metric span {
  display: inline;
  color: var(--muted);
  font-size: 0.72rem;
}

.area-mini-graph-card,
.area-card-list {
  padding: 12px 0 0;
  margin-bottom: 14px;
  border-top: 1px solid var(--border);
}

.section-heading-row {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 12px;
  margin-bottom: 8px;
}

.area-mini-graph {
  width: 100%;
  height: 260px;
  display: block;
  margin-top: 4px;
  overflow: visible;
}

.area-mini-edge {
  fill: none;
  stroke: #64748b;
  stroke-width: 1.0;
  stroke-opacity: 0.34;
}

.area-mini-edge.semantic {
  stroke-width: 1.35;
  stroke-opacity: 0.54;
}

.area-mini-node {
  cursor: pointer;
}

.area-mini-node-box {
  fill: #ffffff;
  stroke: #cbd5e1;
  stroke-width: 1.1;
  rx: 0;
}

.area-mini-node-strip {
  stroke: none;
}

.area-mini-node.active .area-mini-node-box,
.area-mini-node:hover .area-mini-node-box {
  stroke: var(--area-color, #111827);
  stroke-width: 2;
}

.area-mini-node text {
  font-size: 9px;
  font-weight: 650;
  fill: #111827;
  stroke: none;
  pointer-events: none;
}

.area-card-grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(320px, 1fr));
  gap: 6px;
}

.area-overview-card {
  width: 100%;
  display: block;
  text-align: left;
  border: 1px solid var(--border);
  border-left: 5px solid var(--area-color, var(--border-strong));
  background: #fff;
  border-radius: 0;
  padding: 0;
  overflow: hidden;
  cursor: pointer;
  font: inherit;
}

.area-overview-card:hover,
.area-overview-card.active {
  border-color: var(--border-strong);
  border-left-color: var(--area-color, var(--border-strong));
  background: #fbfbfb;
}

.area-card-main {
  min-width: 0;
  padding: 8px 10px;
}

.area-card-title-row {
  display: flex;
  align-items: baseline;
  justify-content: space-between;
  gap: 10px;
}

.area-card-title-row strong {
  font-size: 0.9rem;
  font-weight: 650;
}

.area-card-counts {
  color: var(--muted);
  font-size: 0.72rem;
  white-space: nowrap;
}

.area-card-main p {
  margin: 4px 0 5px;
  color: #334155;
  line-height: 1.36;
  font-size: 0.82rem;
  overflow: visible;
}

.area-card-meta {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
  align-items: center;
  margin-top: 5px;
  overflow: visible;
}

.area-card-meta span,
.area-card-meta code {
  border: 1px solid var(--border);
  background: var(--surface-subtle);
  color: #475569;
  padding: 1px 5px;
  font-size: 0.7rem;
  font-style: normal;
}

.area-card-meta span:first-child {
  color: #334155;
  font-weight: 650;
}



/* Project overview refinements */
.overview-block li .mathjax-inline,
.overview-block li .math-fallback {
  font-size: 0.96em;
}
.area-overview-card {
  overflow: visible;
}

/* Project overview: use the page/column scroll, not a nested scrollbar. */
.area-card-list {
  max-height: none;
  overflow: visible;
}

.overview-goal .mathjax-inline,
.overview-goal .math-fallback {
  font-size: 0.96em;
}

.graph-shell.has-blueprint-reader {
  grid-template-rows: auto auto minmax(180px, calc((var(--sidebar-top-fr, 55) * 1vh) - 84px)) minmax(240px, 1fr);
}

.blueprint-reader-panel {
  min-height: 0;
  overflow: auto;
  border-top: 1px solid var(--border);
  background: #ffffff;
  padding: 16px 18px 20px;
  display: grid;
  gap: 14px;
  align-content: start;
}

.blueprint-reader-simple {
  font-family: ui-serif, Georgia, Cambria, "Times New Roman", Times, serif;
}

.blueprint-reader-empty {
  min-height: 150px;
  display: flex;
  align-items: flex-start;
  color: var(--muted);
  font-family: var(--sans);
}

.blueprint-reader-empty p {
  margin: 7px 0 0;
}

.blueprint-reader-label {
  font-family: var(--sans);
  color: #334155;
  font-size: 0.76rem;
  font-weight: 750;
  text-transform: uppercase;
  letter-spacing: 0.055em;
  margin-bottom: 10px;
}

.blueprint-math-card {
  border-left: 2px solid #0f172a;
  padding: 2px 0 2px 18px;
  background: #ffffff;
}

.blueprint-latex-block {
  color: #0f172a;
  font-size: 1.06rem;
  line-height: 1.65;
  white-space: normal;
  overflow-wrap: normal;
}

.blueprint-latex-block p {
  margin: 0.45em 0;
}

.blueprint-latex-block.statement {
  font-size: 1.12rem;
}

.blueprint-latex-block.proof {
  color: #1f2937;
  font-size: 1rem;
}

.blueprint-match-token {
  border-radius: 4px;
  box-decoration-break: clone;
  -webkit-box-decoration-break: clone;
  cursor: crosshair;
  padding: 0.08em 0.16em;
  text-decoration: none;
  background: rgba(56, 189, 248, 0.22);
}

.blueprint-match-token:hover,
.blueprint-match-token:focus,
.blueprint-match-token.active {
  background: rgba(250, 204, 21, 0.42);
  outline: none;
}

.blueprint-display-match-token {
  display: block;
  padding: 8px 10px;
}

.file-line.blueprint-granular-line-highlight .file-line-code,
.file-line.blueprint-granular-line-highlight .file-line-number {
  background: rgba(250, 204, 21, 0.32) !important;
}

.file-line.blueprint-granular-line-highlight {
  border-left-color: #ca8a04 !important;
}

.blueprint-latex-list {
  margin: 0.6em 0 0.6em 1.35em;
  padding-left: 1.15em;
}

.blueprint-latex-list li {
  margin: 0.35em 0;
  padding-left: 0.15em;
}

.blueprint-latex-block mjx-container[jax="SVG"] {
  max-width: 100%;
  overflow-x: auto;
  overflow-y: hidden;
}

.blueprint-latex-block mjx-container[display="true"] {
  margin: 0.65em 0;
}

.blueprint-display-math {
  margin: 0.65em 0;
  overflow-x: auto;
  overflow-y: hidden;
}

.blueprint-reader-panel:not(.mathjax-ready) .blueprint-latex-block {
  font-family: ui-serif, Georgia, Cambria, "Times New Roman", Times, serif;
}

.paper-shell {
  grid-template-rows: auto auto 1fr;
}

.paper-combined-shell {
  grid-template-rows: auto minmax(0, 1fr);
  position: relative;
}

.paper-combined-split {
  --paper-graph-percent: 48%;
  --paper-analysis-height: var(--paper-graph-percent);
  min-height: 0;
  height: 100%;
  display: grid;
  grid-template-rows: minmax(0, 1fr) 6px minmax(220px, var(--paper-analysis-height));
  background: #f6f7f9;
}

.paper-combined-split.paper-analysis-collapsed {
  grid-template-rows: minmax(0, 1fr) 0 48px;
}

.paper-combined-split.paper-analysis-collapsed .paper-vertical-splitter {
  min-height: 0;
  height: 0;
  overflow: hidden;
  border: 0;
  pointer-events: none;
}

.paper-combined-split.paper-analysis-collapsed .paper-graph-pane {
  border-top: 1px solid var(--border);
}

.paper-graph-pane {
  min-height: 0;
  position: relative;
  display: grid;
  grid-template-rows: auto minmax(0, 1fr);
  overflow: hidden;
  background: #fff;
}

.paper-graph-toolbar {
  min-height: 36px;
  padding-top: 5px;
  padding-bottom: 5px;
}

.paper-graph-canvas {
  min-height: 0;
  border-top: 1px solid var(--border);
}

.paper-vertical-splitter {
  position: relative;
  min-height: 6px;
  cursor: row-resize;
  background: #f6f7f9;
  border-top: 1px solid var(--border);
  border-bottom: 1px solid var(--border);
  z-index: 8;
}

.paper-vertical-splitter::after {
  content: '';
  position: absolute;
  inset: -3px 0;
}

.paper-vertical-splitter span {
  display: none;
}

.paper-vertical-splitter:hover {
  background: #eef2f7;
}

.paper-pdf-pane {
  min-height: 0;
  overflow: hidden;
  background: #eef1f5;
}

.paper-toolbar {
  min-height: 54px;
  padding: 9px 12px;
  border-bottom: 1px solid var(--border);
  background: var(--surface-subtle);
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 12px;
}

.paper-compact-toolbar {
  min-height: 44px;
  padding: 7px 10px;
  background: #ffffff;
}

.paper-toolbar-main.compact {
  display: flex;
  align-items: center;
  min-width: 0;
}

.paper-toolbar-main {
  min-width: 0;
  display: grid;
  gap: 2px;
}

.paper-toolbar-title {
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
  font-weight: 650;
  font-size: 0.95rem;
}

.paper-toolbar-subtitle {
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
  color: var(--muted);
  font-size: 0.82rem;
}

.paper-toolbar-actions {
  display: flex;
  align-items: center;
  gap: 8px;
  flex-shrink: 0;
}

.paper-open-link {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  text-decoration: none;
}

.paper-viewer {
  min-height: 0;
  overflow: hidden;
  background: #eef1f5;
}

.paper-pdf-js-viewer {
  height: 100%;
  min-height: 0;
  display: grid;
  grid-template-rows: auto auto 1fr;
}

.paper-toolbar-title-row {
  min-width: 0;
  display: flex;
  align-items: center;
  gap: 10px;
}

.paper-view-switch {
  display: inline-flex;
  align-items: center;
  gap: 2px;
  padding: 2px;
  border: 1px solid #dbe3ee;
  border-radius: 999px;
  background: #f8fafc;
  flex-shrink: 0;
}

.paper-view-switch-button {
  border: 0;
  border-radius: 999px;
  padding: 4px 10px;
  background: transparent;
  color: #64748b;
  font: inherit;
  font-size: 0.78rem;
  font-weight: 750;
  line-height: 1;
  cursor: pointer;
}

.paper-view-switch-button.active {
  background: #111827;
  color: #ffffff;
  box-shadow: 0 1px 2px rgba(15, 23, 42, 0.18);
}

.paper-view-switch-button:disabled {
  opacity: 0.45;
  cursor: not-allowed;
}


.paper-html-preload-host {
  position: fixed;
  left: -10000px;
  top: 0;
  width: 920px;
  max-width: 920px;
  visibility: hidden;
  pointer-events: none;
  z-index: -1;
}

.paper-html-viewer {
  height: 100%;
  min-height: 0;
  display: grid;
  grid-template-rows: auto 1fr;
  background: #eeeeee;
}

.paper-html-toolbar .paper-toolbar-main.compact {
  display: grid;
  gap: 2px;
}

.paper-html-main {
  position: relative;
  min-height: 0;
  display: grid;
  grid-template-columns: minmax(0, 1fr) 16px;
}

.paper-html-scroll {
  min-height: 0;
  overflow: auto;
  padding: 10px 8px 22px 10px;
}

.paper-html-document {
  width: min(1120px, calc(100% - 12px));
  margin: 0 auto;
  padding: 32px 38px 46px;
  border: 1px solid #cfcfcf;
  border-radius: 0;
  background: #ffffff;
  box-shadow: none;
  color: #151515;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 1.03rem;
  line-height: 1.64;
}

.paper-html-header {
  margin-bottom: 30px;
  padding-bottom: 22px;
  border-bottom: 1px solid #d8d8d8;
  text-align: center;
}

.paper-html-header h1 {
  margin: 0;
  color: #111111;
  font-size: clamp(1.75rem, 3vw, 2.35rem);
  font-weight: 600;
  line-height: 1.16;
  letter-spacing: 0;
}

.paper-html-authors {
  margin-top: 14px;
  color: #333333;
  font-size: 1rem;
}

.paper-html-abstract {
  margin: 24px 0 34px;
  padding: 0 0 20px;
  border: none;
  border-bottom: 1px solid #d8d8d8;
  border-radius: 0;
  background: transparent;
}

.paper-html-abstract h2 {
  margin: 0 0 10px;
  color: #111111;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 1rem;
  font-weight: 700;
  letter-spacing: 0;
  text-transform: none;
  text-align: center;
}

.paper-html-abstract p,
.paper-html-paragraph-block p,
.paper-html-statement p,
.paper-html-proof-body p,
.paper-html-step-body p {
  margin: 0 0 0.82em;
  text-align: justify;
  text-justify: inter-word;
  hyphens: auto;
}

.paper-html-abstract p:last-child,
.paper-html-paragraph-block p:last-child,
.paper-html-statement p:last-child,
.paper-html-proof-body p:last-child,
.paper-html-step-body p:last-child {
  margin-bottom: 0;
}

.paper-html-section-heading {
  margin: 38px 0 14px;
  scroll-margin-top: 22px;
}

.paper-html-section-path {
  display: none;
}

.paper-html-section-heading h2,
.paper-html-section-heading h3,
.paper-html-section-heading h4,
.paper-html-section-heading h5 {
  margin: 0;
  color: #111111;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-weight: 700;
  line-height: 1.22;
  letter-spacing: 0;
}

.paper-html-section-heading h2 { font-size: 1.38rem; }
.paper-html-section-heading h3 { font-size: 1.18rem; }
.paper-html-section-heading h4 { font-size: 1.06rem; }
.paper-html-section-heading h5 { font-size: 1rem; }

.paper-html-paragraph-block {
  margin: 11px 0;
}

.paper-html-item,
.paper-html-step,
.paper-html-equation,
.paper-html-proof {
  position: relative;
  margin: 16px 0;
  scroll-margin-top: 18px;
}

.paper-html-item {
  display: block;
  overflow: visible;
  border: 1px solid #cfcfcf;
  border-left: 4px solid #777777;
  border-radius: 0;
  background: #ffffff;
  box-shadow: none;
  transition: border-color 140ms ease, background-color 140ms ease;
}

.paper-html-clickable {
  cursor: pointer;
}

.paper-html-clickable:hover {
  background: #f7f7f7;
}

.paper-html-clickable:focus-visible {
  outline: 2px solid #111111;
  outline-offset: 2px;
}

.paper-html-item.selected,
.paper-html-step.selected,
.paper-html-equation.selected,
.paper-html-proof.selected,
.paper-html-paragraph-block.selected {
  box-shadow: none;
  transform: none;
}

.paper-html-item.paper-html-kind-theorem { border-left-color: #2563eb; }
.paper-html-item.paper-html-kind-lemma { border-left-color: #7c3aed; }
.paper-html-item.paper-html-kind-proposition,
.paper-html-item.paper-html-kind-prop { border-left-color: #a16207; }
.paper-html-item.paper-html-kind-corollary { border-left-color: #0369a1; }
.paper-html-item.paper-html-kind-definition,
.paper-html-item.paper-html-kind-def { border-left-color: #047857; }
.paper-html-item.paper-html-kind-conjecture { border-left-color: #991b1b; }

.paper-html-item.paper-html-kind-theorem:hover { background: #f5f8ff; border-color: #2563eb; }
.paper-html-item.paper-html-kind-lemma:hover { background: #f8f5ff; border-color: #7c3aed; }
.paper-html-item.paper-html-kind-proposition:hover,
.paper-html-item.paper-html-kind-prop:hover { background: #fffaf0; border-color: #a16207; }
.paper-html-item.paper-html-kind-corollary:hover { background: #f0f9ff; border-color: #0369a1; }
.paper-html-item.paper-html-kind-definition:hover,
.paper-html-item.paper-html-kind-def:hover { background: #f0fdf4; border-color: #047857; }
.paper-html-item.paper-html-kind-conjecture:hover { background: #fef2f2; border-color: #991b1b; }

.paper-html-item.selected {
  border-left-width: 6px;
}

.paper-html-item.paper-html-kind-theorem.selected { background: #f5f8ff; border-color: #2563eb; }
.paper-html-item.paper-html-kind-lemma.selected { background: #f8f5ff; border-color: #7c3aed; }
.paper-html-item.paper-html-kind-proposition.selected,
.paper-html-item.paper-html-kind-prop.selected { background: #fffaf0; border-color: #a16207; }
.paper-html-item.paper-html-kind-corollary.selected { background: #f0f9ff; border-color: #0369a1; }
.paper-html-item.paper-html-kind-definition.selected,
.paper-html-item.paper-html-kind-def.selected { background: #f0fdf4; border-color: #047857; }
.paper-html-item.paper-html-kind-conjecture.selected { background: #fef2f2; border-color: #991b1b; }

.paper-html-item.selected .paper-html-item-title,
.paper-html-step.selected .paper-html-step-title,
.paper-html-equation.selected .paper-html-equation-label {
  font-weight: 750;
}

.paper-html-paragraph-block.selected {
  background: #f8fafc;
  outline: 2px solid #111111;
  outline-offset: 4px;
}

.paper-html-item-main {
  padding: 13px 16px 15px;
}

.paper-html-item-topline {
  display: flex;
  align-items: baseline;
  flex-wrap: wrap;
  gap: 6px;
  margin-bottom: 8px;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
}

.paper-html-kind-label {
  border-radius: 0;
  padding: 0;
  background: transparent;
  color: #111111;
  font-size: 1rem;
  font-weight: 700;
  letter-spacing: 0;
  text-transform: none;
}

.paper-html-item-title {
  color: #111111;
  font-size: 1rem;
  font-weight: 700;
}

.paper-html-status-wrap {
  position: relative;
  display: inline-flex;
  align-items: center;
  margin-left: auto;
}

.paper-html-status-text {
  display: inline-flex;
  align-items: center;
  gap: 5px;
  margin-left: 0;
  padding: 2px 7px;
  border: 1px solid #d6d6d6;
  background: #fafafa;
  color: #444444;
  font-family: var(--mono);
  font-size: 0.78rem;
  font-weight: 700;
  letter-spacing: 0.005em;
  white-space: nowrap;
}

.paper-html-status-tooltip {
  position: absolute;
  z-index: 20;
  top: calc(100% + 8px);
  right: 0;
  width: min(370px, calc(100vw - 56px));
  max-height: 320px;
  overflow: auto;
  display: grid;
  gap: 8px;
  padding: 11px 12px 12px;
  border: 1px solid #c7c7c7;
  background: #ffffff;
  color: #1f2328;
  box-shadow: 0 12px 28px rgba(15, 23, 42, 0.14);
  font-family: Inter, ui-sans-serif, system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 0.78rem;
  line-height: 1.35;
  text-align: left;
  opacity: 0;
  pointer-events: none;
  transform: translateY(-2px);
  transition: opacity 120ms ease, transform 120ms ease;
}

.paper-html-status-tooltip::before {
  content: "";
  position: absolute;
  top: -5px;
  right: 18px;
  width: 9px;
  height: 9px;
  border-left: 1px solid #c7c7c7;
  border-top: 1px solid #c7c7c7;
  background: #ffffff;
  transform: rotate(45deg);
}

.paper-html-status-wrap:hover .paper-html-status-tooltip,
.paper-html-status-wrap:focus-within .paper-html-status-tooltip {
  opacity: 1;
  pointer-events: auto;
  transform: translateY(0);
}

.paper-status-tooltip-kicker,
.paper-status-tooltip-target > span,
.paper-status-tooltip-meta,
.paper-status-tooltip-judgment {
  font-family: var(--mono);
}

.paper-status-tooltip-kicker {
  color: #6b7280;
  font-size: 0.66rem;
  font-weight: 800;
  letter-spacing: 0.04em;
  text-transform: uppercase;
}

.paper-status-tooltip-target {
  display: grid;
  gap: 3px;
}

.paper-status-tooltip-target > span {
  color: #525252;
  font-size: 0.7rem;
  font-weight: 800;
}

.paper-status-tooltip-target code {
  min-width: 0;
  padding: 3px 5px;
  border: 1px solid #e5e7eb;
  background: #f8fafc;
  color: #111827;
  font-family: var(--mono);
  font-size: 0.76rem;
  line-height: 1.35;
  white-space: normal;
  overflow-wrap: anywhere;
}

.paper-status-tooltip-meta,
.paper-status-tooltip-judgment {
  color: #475569;
  font-size: 0.7rem;
  font-weight: 700;
}

.paper-status-tooltip-explanation {
  color: #2f343b;
}

.paper-html-status-icon {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  min-width: 1.05em;
  font-size: 0.86rem;
  line-height: 1;
}
.paper-html-status-blueprint_only .paper-html-status-icon {
  min-width: 1.7em;
  font-size: 0.72rem;
}
.paper-html-status-partial .paper-html-status-icon,
.paper-match-partial .paper-match-status-icon,
.paper-coverage-status-partial span:first-child,
.paper-coverage-filter-partial .paper-coverage-filter-icon {
  position: relative;
  font-size: 0;
}
.paper-html-status-partial .paper-html-status-icon {
  width: 13px;
  min-width: 13px;
  height: 13px;
  border-radius: 999px;
  background: #d97706;
}
.paper-html-status-partial .paper-html-status-icon::before,
.paper-match-partial .paper-match-status-icon::before,
.paper-coverage-status-partial span:first-child::before,
.paper-coverage-filter-partial .paper-coverage-filter-icon::before {
  content: "";
  position: absolute;
  left: 50%;
  top: 50%;
  width: 9px;
  height: 9px;
  border-radius: 999px;
  background: transparent;
  border: 1.5px solid #ffffff;
  transform: translate(-50%, -50%);
  box-sizing: border-box;
}
.paper-html-status-partial .paper-html-status-icon::after,
.paper-match-partial .paper-match-status-icon::after,
.paper-coverage-status-partial span:first-child::after,
.paper-coverage-filter-partial .paper-coverage-filter-icon::after {
  content: "";
  position: absolute;
  left: 50%;
  top: 50%;
  width: 1.5px;
  height: 9px;
  border-radius: 999px;
  background: #ffffff;
  transform: translate(-50%, -50%);
}

.paper-html-status-formalized .paper-html-status-text { color: #14532d; border-color: #86efac; background: #f0fdf4; }
.paper-html-status-statement_only .paper-html-status-text { color: #3f6212; border-color: #bef264; background: #f7fee7; }
.paper-html-status-partial .paper-html-status-text,
.paper-html-status-incomplete .paper-html-status-text,
.paper-html-status-structural .paper-html-status-text { color: #6a4b00; border-color: #d7bd72; background: #fffaf0; }
.paper-html-status-blueprint_only .paper-html-status-text { color: #1d4ed8; border-color: #bfdbfe; background: #eff6ff; }
.paper-html-status-not_locally_formalized .paper-html-status-text,
.paper-html-status-missing .paper-html-status-text,
.paper-html-status-unresolved .paper-html-status-text,
.paper-html-status-review .paper-html-status-text,
.paper-html-status-auxiliary .paper-html-status-text { color: #6b1f1f; border-color: #d3a6a6; background: #fff7f7; }

.paper-html-statement {
  color: #151515;
}

.paper-html-step {
  padding: 13px 16px;
  border: 1px solid #d4d4d4;
  border-radius: 0;
  background: #ffffff;
  box-shadow: none;
}

.paper-html-step-title {
  margin-bottom: 7px;
  color: #111111;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 1rem;
  font-weight: 700;
}

.paper-html-equation {
  padding: 10px 14px;
  border-radius: 0;
  background: transparent;
  text-align: center;
}

.paper-html-equation-label {
  margin-bottom: 6px;
  color: #555555;
  font-family: var(--mono);
  font-size: 0.72rem;
}

.paper-html-proof {
  margin-top: -4px;
  padding: 12px 16px 14px;
  border-left: 2px solid #b8b8b8;
  background: #fafafa;
  color: #222222;
}

.paper-html-proof-label {
  margin-bottom: 6px;
  color: #111111;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 1rem;
  font-weight: 700;
  letter-spacing: 0;
  text-transform: none;
}

.paper-html-cite,
.paper-html-ref {
  border-radius: 0;
  padding: 0 1px;
  background: #eef2ff;
  color: #1d3f8f;
  border-bottom: 1px solid rgba(29, 63, 143, 0.35);
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 1em;
  font-weight: 400;
  text-decoration: none;
}

.paper-html-cite:hover,
.paper-html-ref:hover {
  background: #dbeafe;
  color: #111111;
}

.paper-html-document .MathJax,
.paper-html-document mjx-container {
  font-size: 102% !important;
}


.paper-html-minimap {
  position: relative;
  min-height: 0;
  width: 16px;
  background: #f3f3f3;
  border-left: 1px solid #d4d4d4;
  overflow: hidden;
}

.paper-html-minimap-track {
  position: absolute;
  inset: 8px 3px;
  background: #e5e5e5;
  overflow: hidden;
}

.paper-html-minimap-segment {
  position: absolute;
  left: 0;
  right: 0;
  z-index: 1;
  display: block;
  border: 0;
  padding: 0;
  margin: 0;
  cursor: pointer;
  opacity: 0.66;
}

.paper-html-minimap-segment:hover,
.paper-html-minimap-segment.active {
  opacity: 1;
}

.paper-html-minimap-segment.active {
  box-shadow: inset 0 0 0 1px #111111;
}

.paper-html-minimap-kind-theorem { background: #2563eb; }
.paper-html-minimap-kind-lemma { background: #7c3aed; }
.paper-html-minimap-kind-proposition,
.paper-html-minimap-kind-prop { background: #a16207; }
.paper-html-minimap-kind-corollary { background: #0369a1; }
.paper-html-minimap-kind-definition,
.paper-html-minimap-kind-def { background: #047857; }
.paper-html-minimap-kind-conjecture { background: #991b1b; }
.paper-html-minimap-kind-step { background: #525252; }
.paper-html-minimap-kind-equation { background: #737373; }
.paper-html-minimap-kind-other { background: #8a8a8a; }

.paper-html-minimap-viewport {
  position: absolute;
  left: -1px;
  right: -1px;
  top: 0;
  z-index: 3;
  min-height: 18px;
  border: 1px solid #111111;
  background: rgba(255, 255, 255, 0.18);
  pointer-events: none;
}

@media (max-width: 980px) {
  .paper-html-main {
    grid-template-columns: minmax(0, 1fr);
  }
  .paper-html-minimap {
    display: none;
  }
  .paper-html-scroll {
    padding: 8px 6px 18px;
  }
  .paper-html-document {
    width: min(100%, calc(100% - 8px));
    padding: 24px 22px 34px;
  }
  .paper-toolbar-title-row {
    flex-wrap: wrap;
  }
}

.paper-pdf-controls {
  min-height: 44px;
  padding: 7px 10px;
  display: flex;
  align-items: center;
  justify-content: center;
  gap: 10px;
  flex-wrap: wrap;
  border-bottom: 1px solid var(--border);
  background: #ffffff;
}

.paper-pdf-controls.compact-inline {
  min-height: 0;
  padding: 0;
  border-bottom: none;
  background: transparent;
  justify-content: flex-end;
  flex-wrap: nowrap;
  flex-shrink: 0;
}

.paper-page-control {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  gap: 6px;
  color: var(--muted);
  font-size: 0.82rem;
}

.paper-page-input {
  width: 64px;
  min-height: 30px;
  border: 1px solid var(--border);
  border-radius: 8px;
  padding: 3px 7px;
  font: inherit;
  color: var(--text);
  background: #fff;
  text-align: center;
}

.paper-page-total,
.paper-zoom-label {
  color: var(--muted);
  font-size: 0.82rem;
  min-width: 44px;
  text-align: center;
  display: inline-flex;
  align-items: center;
  justify-content: center;
}

.paper-control-separator {
  width: 1px;
  height: 24px;
  background: var(--border);
  margin: 0 2px;
}

.paper-pdf-status {
  padding: 7px 12px;
  border-bottom: 1px solid var(--border);
  background: #f8fafc;
  color: var(--muted);
  font-size: 0.82rem;
}

.paper-pdf-status.error {
  color: #991b1b;
  background: #fef2f2;
  border-bottom-color: #fecaca;
}

.paper-pdf-status.hidden {
  display: none;
}

.paper-pdf-scroll {
  min-height: 0;
  overflow: auto;
  padding: 22px 18px 34px;
  background: #e8edf3;
}

.paper-pages-container {
  width: 100%;
  display: flex;
  flex-direction: column;
  align-items: center;
  gap: 22px;
}

.paper-page-shell {
  position: relative;
  background: #fff;
  box-shadow: 0 12px 32px rgba(15, 23, 42, 0.18);
  border-radius: 2px;
  overflow: hidden;
  flex: 0 0 auto;
}

.paper-page-shell.rendered {
  background: #fff;
}

.paper-page-label {
  position: absolute;
  top: 8px;
  left: 8px;
  z-index: 4;
  padding: 3px 7px;
  border-radius: 999px;
  background: rgba(15, 23, 42, 0.58);
  color: #fff;
  font-size: 0.7rem;
  line-height: 1.2;
  opacity: 0;
  pointer-events: none;
  transition: opacity 0.15s ease;
}

.paper-page-shell:hover .paper-page-label {
  opacity: 1;
}

.paper-page-loading {
  position: absolute;
  inset: 0;
  display: grid;
  place-items: center;
  color: var(--muted);
  background: #fff;
  font-size: 0.84rem;
  z-index: 3;
}

.paper-pdf-canvas {
  display: block;
  background: #fff;
  image-rendering: auto;
}

.paper-text-layer {
  position: absolute;
  inset: 0;
  overflow: hidden;
  opacity: 1;
  line-height: 1;
  text-align: initial;
  transform-origin: 0 0;
  z-index: 2;
  user-select: text;
}

.paper-text-layer span,
.paper-text-layer br {
  position: absolute;
  color: transparent;
  white-space: pre;
  cursor: text;
  transform-origin: 0% 0%;
}

.paper-text-layer span {
  forced-color-adjust: none;
}

.paper-text-layer ::selection {
  background: rgba(37, 99, 235, 0.28);
  color: transparent;
}

/* Paper item highlight — rendered as <div> rectangles inside each page's
 * .paper-overlay-layer (a non-interactive layer that sits above the canvas
 * and the text layer). One <div> per visual line of the selected item.
 * Drawn this way rather than as text-layer span backgrounds because each
 * pdf.js span is a single word or formula symbol, which would make the
 * highlight look picket-fence shaped, especially around math.
 */
.paper-highlight-overlay {
  position: absolute;
  pointer-events: none;
  border-radius: 3px;
  background-color: rgba(250, 204, 21, 0.38);
  /* A soft outer glow gives the band a "marker" feel without a hard edge. */
  box-shadow: 0 0 0 1px rgba(202, 138, 4, 0.18);
  transition: opacity 120ms ease-out;
}

.paper-highlight-band-proof {
  background-color: rgba(250, 204, 21, 0.16);
  box-shadow: 0 0 0 1px rgba(202, 138, 4, 0.08);
}

.paper-overlay-layer {
  position: absolute;
  inset: 0;
  pointer-events: none;
  z-index: 3;
}

.paper-overlay-empty {
  position: absolute;
  top: 10px;
  right: 10px;
  padding: 4px 8px;
  border-radius: 999px;
  background: rgba(15, 23, 42, 0.62);
  color: #fff;
  font-size: 0.72rem;
  letter-spacing: 0.01em;
  opacity: 0.65;
}

.paper-highlight {
  position: absolute;
  border: 2px solid rgba(37, 99, 235, 0.75);
  background: rgba(37, 99, 235, 0.12);
  border-radius: 6px;
}


.hidden {
  display: none !important;
}

.navigator-switch {
  display: inline-flex;
  align-items: center;
  border: 1px solid var(--border);
  background: #f6f8fa;
  height: 26px;
}

.navigator-switch-button {
  border: none;
  background: transparent;
  color: var(--muted);
  font: inherit;
  font-size: 0.74rem;
  height: 24px;
  padding: 0 8px;
  cursor: pointer;
}

.navigator-switch-button.active {
  background: #fff;
  color: var(--text);
  font-weight: 600;
  box-shadow: inset 0 0 0 1px var(--border-strong);
}

.paper-nav-summary {
  padding: 9px 12px 8px;
  border-bottom: 1px solid var(--border);
  background: #fafafa;
}

.paper-nav-title {
  font-size: 0.82rem;
  font-weight: 600;
  margin-bottom: 4px;
}

.paper-nav-meta {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
  color: var(--muted);
  font-size: 0.72rem;
}

.paper-nav-meta span {
  border: 1px solid var(--border);
  background: #fff;
  padding: 1px 5px;
}

.paper-tree-line {
  grid-template-columns: auto auto minmax(0, 1fr) auto;
}

.paper-section-row {
  font-weight: 500;
}

.paper-entry-row {
  cursor: default;
  color: #374151;
}

.paper-entry-row:hover {
  background: transparent;
}

.paper-section-icon,
.paper-entry-icon {
  width: 16px;
  height: 16px;
  display: inline-flex;
  align-items: center;
  justify-content: center;
  border-radius: 999px;
  font-size: 0.62rem;
  font-weight: 700;
  flex: 0 0 auto;
}

.paper-section-icon {
  color: #475569;
  background: #f1f5f9;
  border: 1px solid #e2e8f0;
}

.paper-entry-icon {
  color: #334155;
  background: #fff;
  border: 1px solid var(--border-strong);
}

.paper-entry-theorem { color: #1d4ed8; border-color: #bfdbfe; background: #eff6ff; }
.paper-entry-lemma { color: #6d28d9; border-color: #ddd6fe; background: #f5f3ff; }
.paper-entry-prop { color: #047857; border-color: #a7f3d0; background: #ecfdf5; }
.paper-entry-cor { color: #9a3412; border-color: #fed7aa; background: #fff7ed; }
.paper-entry-step { color: #0f766e; border-color: #99f6e4; background: #f0fdfa; }

.paper-entry-name {
  font-size: 0.82rem;
  color: #475569;
}

.paper-inline-stats {
  gap: 6px;
  font-size: 0.68rem;
}

.paper-label {
  max-width: 84px;
  overflow: hidden;
  text-overflow: ellipsis;
}

/* Paper graph */
.graph-edge.narrative-ref {
  stroke-dasharray: 5 5;
  stroke: #7c3aed;
  stroke-opacity: 0.72;
}

.graph-edge.statement-ref {
  stroke-dasharray: 3 3;
  stroke: #0f766e;
}

.graph-edge.proof-ref {
  stroke: #64748b;
}

.graph-edge.narrative-ref.active,
.graph-edge.narrative-ref.focus-tree,
.graph-edge.statement-ref.active,
.graph-edge.statement-ref.focus-tree,
.graph-edge.proof-ref.active,
.graph-edge.proof-ref.focus-tree {
  stroke-opacity: 0.98;
  stroke-width: 2.35;
}

.paper-entry-row {
  cursor: pointer;
}

.paper-entry-row:hover {
  background: #f8fafc;
}

.paper-focus-block .overview-headline {
  font-size: 0.95rem;
}

.paper-focus-relations {
  display: grid;
  grid-template-columns: 1fr;
  gap: 8px;
}

.paper-relation-list {
  border: 1px solid var(--border);
  background: #fff;
}

.paper-relation-title {
  padding: 6px 8px;
  font-size: 0.72rem;
  font-weight: 700;
  text-transform: uppercase;
  color: var(--muted);
  border-bottom: 1px solid var(--border);
  background: #f8fafc;
}

.paper-relation-item {
  width: 100%;
  display: flex;
  justify-content: space-between;
  align-items: center;
  gap: 8px;
  padding: 7px 8px;
  border: 0;
  border-bottom: 1px solid #f1f5f9;
  background: transparent;
  font: inherit;
  font-size: 0.78rem;
  color: #111827;
  cursor: pointer;
  text-align: left;
}

.paper-relation-item:hover {
  background: #f8fafc;
}

.paper-relation-kind {
  flex: 0 0 auto;
  font-size: 0.64rem;
  color: #64748b;
  border: 1px solid var(--border);
  padding: 1px 5px;
  background: #fff;
}

.paper-statement-preview .paper-statement-text {
  font-size: 0.78rem;
  line-height: 1.45;
  color: #334155;
}

.legend-line.statement-preview {
  border-top: 2px dashed #0f766e;
}

.legend-line.narrative-preview {
  border-top: 2px dashed #7c3aed;
}

@media (max-height: 760px) {
  .paper-combined-split {
    grid-template-rows: minmax(220px, 1fr) 6px minmax(140px, var(--paper-analysis-height));
  }
  .paper-combined-split.paper-analysis-collapsed {
    grid-template-rows: minmax(0, 1fr) 0 48px;
  }
  .paper-graph-toolbar .graph-meta-row {
    gap: 5px;
  }
  .paper-pdf-scroll {
    padding-top: 14px;
  }
}

/* Paper graph: node fill encodes paper item kind; border + badge encode Lean formalization status. */
.graph-node-shape.paper-node-shape {
  stroke: #64748b;
  stroke-width: 2.5;
  stroke-dasharray: none;
  filter: drop-shadow(0 2px 3px rgba(15, 23, 42, 0.11));
}
.graph-node-shape.paper-node-shape.paper-formalization-formalized {
  stroke: #15803d !important;
  stroke-width: 3;
  stroke-dasharray: none;
}
.graph-node-shape.paper-node-shape.paper-formalization-statement_only,
.graph-node-shape.paper-node-shape.paper-formalization-statement {
  stroke: #65a30d !important;
  stroke-width: 3;
  stroke-dasharray: none;
}
.graph-node-shape.paper-node-shape.paper-formalization-partial,
.graph-node-shape.paper-node-shape.paper-formalization-incomplete,
.graph-node-shape.paper-node-shape.paper-formalization-structural {
  stroke: #d97706 !important;
  stroke-width: 3;
  stroke-dasharray: none;
}
.graph-node-shape.paper-node-shape.paper-formalization-blueprint_only {
  stroke: #2563eb !important;
  stroke-width: 3;
  stroke-dasharray: none;
}
.graph-node-shape.paper-node-shape.paper-formalization-not_locally_formalized,
.graph-node-shape.paper-node-shape.paper-formalization-missing,
.graph-node-shape.paper-node-shape.paper-formalization-unresolved,
.graph-node-shape.paper-node-shape.paper-formalization-review,
.graph-node-shape.paper-node-shape.paper-formalization-auxiliary {
  stroke: #dc2626 !important;
  stroke-width: 3.1;
  stroke-dasharray: none;
}
.graph-node-shape.paper-node-shape.paper-formalization-unknown {
  stroke: #64748b !important;
  stroke-width: 2.8;
  stroke-dasharray: none;
}
.graph-node-shape.paper-node-shape.focus,
.graph-node-shape.paper-node-shape.selected-node {
  stroke-width: 4 !important;
}
.paper-status-badge {
  pointer-events: none;
}
.paper-status-badge circle,
.legend-dot.paper-status-preview {
  fill: #64748b;
  stroke: #ffffff;
  stroke-width: 1.5;
}
.paper-status-badge text,
.legend-dot.paper-status-preview span {
  fill: #ffffff;
  color: #ffffff;
  font-size: 12px;
  font-weight: 850;
  line-height: 1;
}
.paper-status-badge .paper-partial-glyph-ring {
  fill: none;
  stroke: #ffffff;
  stroke-width: 1.5;
}
.paper-status-badge .paper-partial-glyph-divider {
  stroke: #ffffff;
  stroke-width: 1.5;
  stroke-linecap: round;
}
.paper-status-badge.paper-badge-formalized circle,
.legend-dot.paper-status-preview.paper-formalization-formalized {
  fill: #15803d;
}
.paper-status-badge.paper-badge-statement_only circle,
.legend-dot.paper-status-preview.paper-formalization-statement_only {
  fill: #65a30d;
}
.paper-status-badge.paper-badge-partial circle,
.paper-status-badge.paper-badge-incomplete circle,
.paper-status-badge.paper-badge-structural circle,
.legend-dot.paper-status-preview.paper-formalization-partial,
.legend-dot.paper-status-preview.paper-formalization-incomplete,
.legend-dot.paper-status-preview.paper-formalization-structural {
  fill: #d97706;
}
.paper-status-badge.paper-badge-blueprint_only circle,
.legend-dot.paper-status-preview.paper-formalization-blueprint_only {
  fill: #2563eb;
}
.paper-status-badge.paper-badge-not_locally_formalized circle,
.paper-status-badge.paper-badge-missing circle,
.paper-status-badge.paper-badge-unresolved circle,
.paper-status-badge.paper-badge-review circle,
.paper-status-badge.paper-badge-auxiliary circle,
.legend-dot.paper-status-preview.paper-formalization-not_locally_formalized,
.legend-dot.paper-status-preview.paper-formalization-missing,
.legend-dot.paper-status-preview.paper-formalization-unresolved,
.legend-dot.paper-status-preview.paper-formalization-review,
.legend-dot.paper-status-preview.paper-formalization-auxiliary {
  fill: #dc2626;
}
.paper-status-badge.paper-badge-unknown circle,
.legend-dot.paper-status-preview.paper-formalization-unknown {
  fill: #64748b;
}
.paper-status-badge.paper-badge-blueprint_only text {
  font-size: 8.5px;
}
.legend-dot.paper-status-preview {
  border-radius: 999px;
  display: inline-grid;
  place-items: center;
  width: 14px;
  height: 14px;
  border: 1.5px solid #ffffff;
  box-shadow: 0 0 0 1px rgba(15, 23, 42, 0.16);
}
.graph-chip.good {
  color: #087f36;
  border-color: rgba(8, 127, 54, 0.25);
  background: #f0fdf4;
}
.graph-chip.warn {
  color: #b45309;
  border-color: rgba(180, 83, 9, 0.28);
  background: #fffbeb;
}

/* Paper formalization map refinements: labels are hidden in the graph, so status badges need to be visually explicit. */
.compact-paper-toolbar .graph-meta-row {
  gap: 6px;
}

.legend-dot.paper-status-preview.paper-formalization-formalized { background: #15803d; }
.legend-dot.paper-status-preview.paper-formalization-statement_only { background: #65a30d; }
.legend-dot.paper-status-preview.paper-formalization-partial,
.legend-dot.paper-status-preview.paper-formalization-incomplete,
.legend-dot.paper-status-preview.paper-formalization-structural { background: #d97706; }
.legend-dot.paper-status-preview.paper-formalization-blueprint_only { background: #2563eb; }
.legend-dot.paper-status-preview.paper-formalization-not_locally_formalized,
.legend-dot.paper-status-preview.paper-formalization-missing,
.legend-dot.paper-status-preview.paper-formalization-unresolved,
.legend-dot.paper-status-preview.paper-formalization-review,
.legend-dot.paper-status-preview.paper-formalization-auxiliary { background: #dc2626; }
.legend-dot.paper-status-preview.paper-formalization-unknown { background: #64748b; }
.legend-dot.paper-status-preview span {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  width: 100%;
  height: 100%;
  color: #fff;
  font-size: 9px;
  font-weight: 850;
  line-height: 1;
}
.legend-dot.paper-status-preview.paper-formalization-blueprint_only span {
  font-size: 7px;
}

.paper-match-card {
  display: grid;
  gap: 8px;
  padding: 10px 12px;
  border-bottom: 1px solid var(--border);
  background: #ffffff;
  box-shadow: 0 1px 0 rgba(15, 23, 42, 0.03);
}
.paper-match-card-header {
  display: flex;
  align-items: flex-start;
  justify-content: space-between;
  gap: 10px;
}

.paper-match-header-actions {
  display: inline-flex;
  align-items: center;
  justify-content: flex-end;
  flex-wrap: wrap;
  gap: 6px;
  flex: 0 0 auto;
}
.paper-match-action {
  border: 1px solid rgba(37, 99, 235, 0.24);
  border-radius: 999px;
  background: #eff6ff;
  color: #1d4ed8;
  padding: 4px 8px;
  font-size: 0.7rem;
  font-weight: 750;
  line-height: 1;
  white-space: nowrap;
  cursor: pointer;
}
.paper-match-action:hover {
  border-color: rgba(37, 99, 235, 0.42);
  background: #dbeafe;
  color: #1e40af;
}
.paper-match-action:focus-visible {
  outline: 2px solid rgba(37, 99, 235, 0.55);
  outline-offset: 1px;
}
.paper-match-title-block {
  min-width: 0;
}
.paper-match-eyebrow,
.paper-match-label {
  color: var(--muted);
  font-size: 0.68rem;
  font-weight: 700;
  letter-spacing: 0.04em;
  text-transform: uppercase;
}
.paper-match-title {
  color: var(--text);
  font-size: 1rem;
  font-weight: 750;
  line-height: 1.15;
}
.paper-match-subtitle {
  margin-top: 2px;
  color: var(--muted);
  font-size: 0.78rem;
  line-height: 1.25;
  overflow-wrap: anywhere;
}
.paper-match-status {
  display: inline-flex;
  align-items: center;
  gap: 5px;
  flex: 0 0 auto;
  padding: 4px 7px;
  border: 1px solid rgba(100, 116, 139, 0.22);
  border-radius: 999px;
  background: #f8fafc;
  color: #334155;
  font-size: 0.72rem;
  font-weight: 750;
  white-space: nowrap;
}
.paper-match-status-icon {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  width: 15px;
  height: 15px;
  border-radius: 999px;
  background: #64748b;
  color: #ffffff;
  font-size: 9px;
  font-weight: 850;
  line-height: 1;
}
.paper-match-formalized .paper-match-status-icon { background: #15803d; }
.paper-match-statement_only .paper-match-status-icon { background: #65a30d; }
.paper-match-partial .paper-match-status-icon,
.paper-match-incomplete .paper-match-status-icon,
.paper-match-structural .paper-match-status-icon { background: #d97706; }
.paper-match-blueprint_only .paper-match-status-icon { background: #2563eb; }
.paper-match-not_locally_formalized .paper-match-status-icon,
.paper-match-missing .paper-match-status-icon,
.paper-match-unresolved .paper-match-status-icon,
.paper-match-review .paper-match-status-icon,
.paper-match-auxiliary .paper-match-status-icon { background: #dc2626; }
.paper-match-blueprint_only .paper-match-status-icon {
  width: 18px;
  font-size: 7px;
}
.paper-match-grid {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
  gap: 8px 12px;
}
.paper-match-value {
  margin-top: 2px;
  color: var(--text);
  font-size: 0.8rem;
  line-height: 1.3;
  overflow-wrap: anywhere;
}
.paper-match-value code {
  font-size: 0.8rem;
}
.paper-match-signature {
  margin: 0;
  max-height: 92px;
  overflow: auto;
  padding: 7px 8px;
  border: 1px solid var(--border);
  border-radius: 8px;
  background: #f8fafc;
  color: #0f172a;
  font-size: 0.74rem;
  line-height: 1.35;
  white-space: pre-wrap;
}
.paper-code-empty-state {
  display: grid;
  place-items: center;
  padding: 18px;
  min-height: 0;
}
.paper-empty-subtext {
  margin-top: 6px;
  color: var(--muted);
  font-size: 0.82rem;
}
.muted-text {
  color: var(--muted);
}

/* Paper graph labels need to be readable from the default fit view. */
.graph-label.inside.paper-node-label {
  fill: #0f172a;
  font-size: 14px;
  font-weight: 750;
  letter-spacing: -0.01em;
  paint-order: normal;
  stroke: none;
  stroke-width: 0;
}
.graph-label.inside.paper-node-label.focus {
  font-weight: 850;
}

.paper-match-card {
  gap: 6px;
  padding: 8px 10px;
}
.paper-match-grid.paper-match-grid-compact {
  grid-template-columns: minmax(0, 1.15fr) minmax(0, 0.75fr) minmax(0, 1fr);
  gap: 6px 10px;
}
.paper-match-grid.paper-match-grid-compact .paper-match-label {
  font-size: 0.62rem;
}
.paper-match-grid.paper-match-grid-compact .paper-match-value,
.paper-match-grid.paper-match-grid-compact .paper-match-value code {
  font-size: 0.76rem;
}

.source-panel-summary.source-panel-summary-compact {
  grid-template-columns: minmax(0, 1fr) auto;
  align-items: center;
  gap: 10px;
  height: 44px;
  min-height: 44px;
  padding: 7px 10px;
  background: #ffffff;
  overflow: hidden;
}
.source-compact-title-block {
  min-width: 0;
  display: grid;
  gap: 2px;
}
.source-panel-summary-compact .source-file-name {
  font-size: 0.95rem;
  line-height: 1.08;
  font-weight: 650;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
  padding-left: 0;
  text-indent: 0;
}
.source-panel-summary-compact .source-summary-text {
  font-size: 0.74rem;
  line-height: 1.15;
  color: #64748b;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}
.source-summary-controls {
  display: inline-flex;
  align-items: center;
  justify-content: flex-end;
  gap: 6px;
  min-width: 0;
  align-self: center;
}
.source-summary-pill {
  flex: 0 0 auto;
  padding: 2px 6px;
  border: 1px solid var(--border);
  border-radius: 999px;
  background: #ffffff;
  color: var(--muted);
  font-size: 0.72rem;
  font-weight: 650;
  white-space: nowrap;
}
.source-panel-summary-compact .source-color-mode {
  margin: 0;
}
.source-panel-summary-compact .file-color-label {
  gap: 5px;
  font-size: 0.72rem;
  flex-wrap: nowrap;
  white-space: nowrap;
}
.source-panel-summary-compact .compact-select {
  height: 24px;
  min-width: 116px;
  font-size: 0.72rem;
  padding-top: 1px;
  padding-bottom: 1px;
}

@media (max-width: 1200px) {
  .paper-match-grid.paper-match-grid-compact {
    grid-template-columns: 1fr;
  }
  .source-panel-summary.source-panel-summary-compact {
    grid-template-columns: 1fr;
  }
  .source-summary-controls {
    justify-content: flex-start;
    flex-wrap: wrap;
  }
}

.paper-llm-assessment {
  display: grid;
  gap: 3px;
  padding: 2px 0 1px;
  border: 0;
  border-radius: 0;
  background: transparent;
}
.paper-llm-heading {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 8px;
}
.paper-llm-kicker {
  color: var(--muted);
  font-size: 0.62rem;
  font-weight: 800;
  letter-spacing: 0.055em;
  text-transform: uppercase;
}
.paper-llm-judgment {
  flex: 0 0 auto;
  padding: 2px 6px;
  border: 1px solid var(--border);
  border-radius: 999px;
  background: #f8fafc;
  color: #334155;
  font-size: 0.68rem;
  font-weight: 750;
  white-space: nowrap;
}
.paper-llm-rationale {
  color: var(--text);
  font-size: 0.76rem;
  line-height: 1.32;
}
.paper-candidates {
  border: 1px solid var(--border);
  border-radius: 9px;
  background: #ffffff;
  overflow: hidden;
}
.paper-candidates > summary {
  cursor: pointer;
  padding: 5px 8px;
  color: var(--muted);
  font-size: 0.66rem;
  font-weight: 800;
  letter-spacing: 0.045em;
  text-transform: uppercase;
  user-select: none;
}
.paper-candidate-list {
  display: grid;
  gap: 0;
  border-top: 1px solid var(--border);
}
.paper-candidate-row {
  display: grid;
  grid-template-columns: 18px minmax(0, 1fr);
  gap: 7px;
  padding: 6px 8px;
  border-top: 1px solid rgba(226, 232, 240, 0.72);
}
.paper-candidate-row:first-child {
  border-top: 0;
}
.paper-candidate-rank {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  width: 18px;
  height: 18px;
  border-radius: 999px;
  background: #f1f5f9;
  color: #475569;
  font-size: 0.64rem;
  font-weight: 850;
}
.paper-candidate-main {
  min-width: 0;
}
.paper-candidate-name {
  color: var(--text);
  font-size: 0.74rem;
  line-height: 1.25;
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
}
.paper-candidate-name code {
  font-size: 0.74rem;
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
}
.paper-candidate-meta {
  margin-top: 1px;
  color: var(--muted);
  font-size: 0.68rem;
  line-height: 1.28;
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
}
.paper-candidate-rationale {
  margin-top: 2px;
  color: #475569;
  font-size: 0.69rem;
  line-height: 1.3;
  white-space: normal;
  overflow: visible;
  overflow-wrap: anywhere;
  word-break: break-word;
}

.paper-html-display-math {
  margin: 0.85em 0;
  overflow-x: auto;
  text-align: center;
}

.paper-html-figure {
  margin: 1.15em auto 1.25em;
  text-align: center;
}

.paper-html-figure img {
  display: block;
  max-width: min(100%, 540px);
  max-height: 360px;
  height: auto;
  margin: 0 auto;
  object-fit: contain;
}

.paper-html-figure figcaption {
  max-width: 620px;
  margin: 0.55em auto 0;
  color: #4a4a4a;
  font-size: 0.9rem;
  line-height: 1.42;
  text-align: center;
}

.paper-html-footnote {
  color: #333333;
  font-size: 0.92em;
}

.paper-html-references {
  margin-top: 42px;
  padding-top: 18px;
  border-top: 1px solid #d8d8d8;
}

.paper-html-references h2 {
  margin: 0 0 14px;
  color: #111111;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 1.24rem;
  font-weight: 700;
  line-height: 1.25;
}

.paper-html-references ol {
  margin: 0;
  padding-left: 2.25em;
}

.paper-html-bibliography-entry {
  margin: 0 0 0.75em;
  padding-left: 0.25em;
  line-height: 1.45;
}

.paper-html-cite,
.paper-html-ref {
  color: #111111;
  text-decoration: none;
  border-bottom: 1px solid #9ca3af;
}

.paper-html-cite:hover,
.paper-html-ref:hover {
  border-bottom-color: #111111;
}

/* Paper coverage table */
.paper-left-mode-header {
  min-height: 36px;
  padding: 5px 10px;
  border-bottom: 1px solid var(--border);
  background: #ffffff;
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 12px;
}

.paper-left-mode-title {
  min-width: 0;
}

.paper-left-mode-actions {
  display: inline-flex;
  align-items: center;
  justify-content: flex-end;
  gap: 8px;
  flex: 0 0 auto;
}

.paper-left-mode-eyebrow {
  color: var(--muted);
  font-size: 0.66rem;
  letter-spacing: 0.08em;
  text-transform: uppercase;
  font-weight: 750;
  margin-bottom: 2px;
}

.paper-left-mode-heading {
  color: #111827;
  font-size: 0.86rem;
  font-weight: 760;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}

.paper-left-mode-switch {
  display: inline-flex;
  align-items: center;
  border: 1px solid var(--border);
  background: #f8fafc;
  flex: 0 0 auto;
}

.paper-left-mode-button {
  border: 0;
  background: transparent;
  color: #64748b;
  height: 25px;
  padding: 0 10px;
  font: inherit;
  font-size: 0.75rem;
  font-weight: 650;
  cursor: pointer;
}

.paper-left-mode-button.active {
  background: #ffffff;
  color: #111827;
  box-shadow: inset 0 0 0 1px var(--border-strong);
}

.paper-left-mode-toggle {
  height: 25px;
  border: 1px solid var(--border);
  background: #ffffff;
  color: #334155;
  padding: 0 9px;
  font: inherit;
  font-size: 0.72rem;
  font-weight: 720;
  cursor: pointer;
  white-space: nowrap;
}

.paper-left-mode-toggle:hover {
  border-color: #94a3b8;
  background: #f8fafc;
}

.paper-graph-toolbar-secondary {
  border-bottom: 1px solid var(--border);
}

.paper-coverage-shell {
  min-height: 0;
  overflow: hidden;
  display: grid;
  grid-template-rows: auto auto minmax(0, 1fr);
  background: #f8fafc;
}

.paper-coverage-summary {
  display: grid;
  grid-template-columns: minmax(0, 1.3fr) minmax(280px, 0.9fr);
  gap: 14px;
  padding: 13px 14px 11px;
  border-bottom: 1px solid var(--border);
  background: #ffffff;
}

.paper-coverage-kicker {
  color: #2563eb;
  font-size: 0.68rem;
  letter-spacing: 0.09em;
  text-transform: uppercase;
  font-weight: 820;
  margin-bottom: 4px;
}

.paper-coverage-summary h2 {
  margin: 0 0 4px;
  font-size: 1.12rem;
  line-height: 1.1;
  color: #0f172a;
}

.paper-coverage-summary p {
  margin: 0;
  max-width: 780px;
  color: #475569;
  font-size: 0.82rem;
  line-height: 1.38;
}

.paper-coverage-metrics {
  display: grid;
  grid-template-columns: repeat(5, minmax(72px, 1fr));
  gap: 6px;
  align-content: start;
}

.paper-coverage-metric {
  background: #f8fafc;
  border: 1px solid var(--border);
  padding: 7px 7px 6px;
  min-width: 0;
}

.paper-coverage-metric-value {
  font-size: 1.06rem;
  line-height: 1;
  font-weight: 820;
  color: #0f172a;
}

.paper-coverage-metric-label {
  margin-top: 4px;
  color: #64748b;
  font-size: 0.64rem;
  line-height: 1.15;
  text-transform: uppercase;
  letter-spacing: 0.04em;
}

.paper-coverage-metric-formalized { border-color: rgba(21, 128, 61, 0.24); background: #f0fdf4; }
.paper-coverage-metric-statement_only { border-color: rgba(101, 163, 13, 0.26); background: #f7fee7; }
.paper-coverage-metric-partial { border-color: rgba(217, 119, 6, 0.26); background: #fffbeb; }
.paper-coverage-metric-blueprint_only { border-color: rgba(37, 99, 235, 0.24); background: #eff6ff; }
.paper-coverage-metric-not_locally_formalized,
.paper-coverage-metric-missing { border-color: rgba(220, 38, 38, 0.2); background: #fef2f2; }

.paper-coverage-controls {
  padding: 9px 12px;
  border-bottom: 1px solid var(--border);
  background: #ffffff;
  display: block;
}

.paper-coverage-filter-row {
  display: flex;
  align-items: center;
  flex-wrap: wrap;
  gap: 6px;
}

.paper-coverage-filter {
  border: 1px solid var(--border);
  background: #ffffff;
  color: #475569;
  padding: 4px 8px;
  font-size: 0.72rem;
  font-weight: 650;
  cursor: pointer;
  display: inline-flex;
  align-items: center;
  gap: 6px;
}

.paper-coverage-filter-icon {
  display: inline-grid;
  place-items: center;
  width: 14px;
  height: 14px;
  border-radius: 999px;
  background: #64748b;
  color: #ffffff;
  font-size: 0.55rem;
  font-weight: 850;
  line-height: 1;
}

.paper-coverage-filter-blueprint_only .paper-coverage-filter-icon {
  width: 18px;
  font-size: 0.42rem;
}

.paper-coverage-filter-formalized .paper-coverage-filter-icon { background: #15803d; }
.paper-coverage-filter-statement_only .paper-coverage-filter-icon { background: #65a30d; }
.paper-coverage-filter-partial .paper-coverage-filter-icon { background: #d97706; }
.paper-coverage-filter-partial .paper-coverage-filter-icon {
  font-size: 0;
}
.paper-coverage-filter-blueprint_only .paper-coverage-filter-icon { background: #2563eb; }
.paper-coverage-filter-not_locally_formalized .paper-coverage-filter-icon { background: #dc2626; }

.paper-coverage-filter strong {
  font-size: 0.68rem;
  color: #64748b;
  font-weight: 760;
}

.paper-coverage-filter.active {
  color: #0f172a;
  border-color: #94a3b8;
  background: #f1f5f9;
}

.paper-coverage-filter-formalized.active {
  border-color: rgba(21, 128, 61, 0.34);
  background: #f0fdf4;
}
.paper-coverage-filter-statement_only.active {
  border-color: rgba(101, 163, 13, 0.34);
  background: #f7fee7;
}
.paper-coverage-filter-partial.active {
  border-color: rgba(217, 119, 6, 0.34);
  background: #fffbeb;
}
.paper-coverage-filter-blueprint_only.active {
  border-color: rgba(37, 99, 235, 0.34);
  background: #eff6ff;
}
.paper-coverage-filter-not_locally_formalized.active {
  border-color: rgba(220, 38, 38, 0.30);
  background: #fef2f2;
}

.paper-coverage-search-wrap {
  display: flex;
  align-items: center;
  gap: 8px;
}

.paper-coverage-search {
  flex: 1 1 auto;
  min-width: 180px;
  height: 30px;
  border: 1px solid var(--border);
  background: #f8fafc;
  color: #0f172a;
  padding: 0 9px;
  font: inherit;
  font-size: 0.78rem;
}

.paper-coverage-search:focus {
  outline: 2px solid rgba(37, 99, 235, 0.20);
  border-color: #93c5fd;
  background: #ffffff;
}

.paper-coverage-count {
  margin-left: auto;
  flex: 0 0 auto;
  color: #64748b;
  font-size: 0.72rem;
  white-space: nowrap;
}

.paper-coverage-table {
  min-height: 0;
  display: grid;
  grid-template-rows: auto minmax(0, 1fr);
  background: #f8fafc;
}

.paper-coverage-table-head {
  display: grid;
  grid-template-columns: minmax(220px, 0.8fr) minmax(320px, 1.1fr) minmax(340px, 1.15fr);
  gap: 0;
  padding: 7px 12px;
  border-bottom: 1px solid var(--border);
  color: #64748b;
  background: #f8fafc;
  font-size: 0.66rem;
  font-weight: 780;
  text-transform: uppercase;
  letter-spacing: 0.06em;
}

.paper-coverage-rows {
  min-height: 0;
  overflow: auto;
  padding-bottom: 12px;
}

.paper-coverage-row {
  display: grid;
  grid-template-columns: minmax(220px, 0.8fr) minmax(320px, 1.1fr) minmax(340px, 1.15fr);
  border-bottom: 1px solid #e5e7eb;
  background: #ffffff;
  cursor: pointer;
}

.paper-coverage-row:hover {
  background: #f8fafc;
}

.paper-coverage-row.selected {
  background: #fffdf5;
  box-shadow: inset 4px 0 0 #f59e0b;
}

.paper-coverage-cell {
  min-width: 0;
  padding: 9px 10px;
  border-right: 1px solid #eef2f7;
  display: grid;
  align-content: start;
  gap: 5px;
  color: #1f2937;
  font-size: 0.76rem;
  line-height: 1.32;
}

.paper-coverage-cell:last-of-type {
  border-right: 0;
}

.paper-coverage-cell-status {
  align-content: start;
}

.paper-coverage-item-title-row {
  display: flex;
  align-items: baseline;
  gap: 7px;
  min-width: 0;
}

.paper-coverage-item-title-row strong {
  min-width: 0;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
  color: #0f172a;
  font-size: 0.82rem;
}

.paper-coverage-kind {
  flex: 0 0 auto;
  border: 1px solid var(--border);
  background: #f8fafc;
  color: #475569;
  padding: 1px 5px;
  font-size: 0.62rem;
  font-weight: 780;
  text-transform: uppercase;
  letter-spacing: 0.04em;
}

.paper-coverage-kind-theorem { color: #1d4ed8; border-color: #bfdbfe; background: #eff6ff; }
.paper-coverage-kind-lemma { color: #6d28d9; border-color: #ddd6fe; background: #f5f3ff; }
.paper-coverage-kind-proposition { color: #047857; border-color: #a7f3d0; background: #ecfdf5; }
.paper-coverage-kind-corollary { color: #9a3412; border-color: #fed7aa; background: #fff7ed; }
.paper-coverage-kind-definition,
.paper-coverage-kind-def { color: #475569; border-color: #cbd5e1; background: #f8fafc; }

.paper-coverage-item-meta,
.paper-coverage-mini-tags {
  display: flex;
  flex-wrap: wrap;
  gap: 5px;
  color: #64748b;
  font-size: 0.68rem;
}

.paper-coverage-item-meta span,
.paper-coverage-mini-tags span,
.paper-coverage-subpill {
  border: 1px solid var(--border);
  background: #f8fafc;
  padding: 1px 5px;
}

.paper-coverage-statement-snippet {
  color: #475569;
  font-size: 0.72rem;
  line-height: 1.35;
  max-height: 2.75em;
  overflow: hidden;
}

.paper-coverage-status-pill {
  width: fit-content;
  display: inline-flex;
  align-items: center;
  gap: 5px;
  border: 1px solid var(--border);
  background: #f8fafc;
  color: #334155;
  padding: 4px 7px;
  font-size: 0.7rem;
  font-weight: 780;
  text-transform: uppercase;
  letter-spacing: 0.03em;
}

.paper-coverage-status-pill span:first-child {
  display: inline-grid;
  place-items: center;
  width: 13px;
  height: 13px;
  border-radius: 999px;
  color: #fff;
  background: #64748b;
  font-size: 0.5rem;
  line-height: 1;
}

.paper-coverage-status-formalized { border-color: rgba(21, 128, 61, 0.28); color: #166534; background: #f0fdf4; }
.paper-coverage-status-formalized span:first-child { background: #15803d; }
.paper-coverage-status-statement_only { border-color: rgba(101, 163, 13, 0.28); color: #3f6212; background: #f7fee7; }
.paper-coverage-status-statement_only span:first-child { background: #65a30d; }
.paper-coverage-status-partial,
.paper-coverage-status-incomplete,
.paper-coverage-status-structural { border-color: rgba(217, 119, 6, 0.28); color: #92400e; background: #fffbeb; }
.paper-coverage-status-partial span:first-child,
.paper-coverage-status-incomplete span:first-child,
.paper-coverage-status-structural span:first-child { background: #d97706; }
.paper-coverage-status-blueprint_only { border-color: rgba(37, 99, 235, 0.28); color: #1d4ed8; background: #eff6ff; }
.paper-coverage-status-blueprint_only span:first-child { background: #2563eb; }
.paper-coverage-status-unknown { border-color: rgba(100, 116, 139, 0.28); color: #475569; background: #f8fafc; }
.paper-coverage-status-unknown span:first-child { background: #64748b; }
.paper-coverage-status-not_locally_formalized,
.paper-coverage-status-missing,
.paper-coverage-status-unresolved,
.paper-coverage-status-auxiliary,
.paper-coverage-status-review { border-color: rgba(220, 38, 38, 0.24); color: #991b1b; background: #fef2f2; }
.paper-coverage-status-not_locally_formalized span:first-child,
.paper-coverage-status-missing span:first-child,
.paper-coverage-status-unresolved span:first-child,
.paper-coverage-status-auxiliary span:first-child,
.paper-coverage-status-review span:first-child { background: #dc2626; }

.paper-coverage-muted-line,
.paper-coverage-empty-cell {
  display: block;
  min-width: 0;
  color: #64748b;
  font-size: 0.7rem;
  overflow: hidden;
  text-overflow: ellipsis;
}

.paper-coverage-empty-cell {
  color: #94a3b8;
  font-style: italic;
}

.paper-coverage-match-name,
.paper-coverage-justification-main {
  min-width: 0;
  color: #0f172a;
  font-size: 0.76rem;
  overflow: hidden;
  text-overflow: ellipsis;
}

.paper-coverage-route-card {
  display: grid;
  gap: 6px;
  min-width: 0;
}

.paper-coverage-route-status-line,
.paper-coverage-route-item,
.paper-coverage-route-reason,
.paper-coverage-route-link,
.paper-coverage-route-secondary {
  display: flex;
  align-items: center;
  gap: 7px;
  min-width: 0;
}

.paper-coverage-route-status-line,
.paper-coverage-route-item,
.paper-coverage-route-link,
.paper-coverage-route-secondary {
  align-items: center;
}

.paper-coverage-route-label {
  flex: 0 0 64px;
  align-self: center;
  color: #64748b;
  font-size: 0.58rem;
  font-weight: 780;
  letter-spacing: 0.045em;
  text-transform: uppercase;
}

.paper-route-status-icon {
  display: inline-grid;
  place-items: center;
  width: 16px;
  height: 16px;
  border-radius: 999px;
  color: #ffffff;
  background: #64748b;
  font-size: 0.58rem;
  line-height: 1;
  font-weight: 850;
}

.paper-route-status {
  gap: 5px;
}

.paper-route-status-exact .paper-route-status-icon { background: #15803d; }
.paper-route-status-partial .paper-route-status-icon { background: #d97706; }
.paper-route-status-related.paper-route-status-blueprint .paper-route-status-icon { background: #2563eb; }
.paper-route-status-related.paper-route-status-lean .paper-route-status-icon { background: #65a30d; }
.paper-route-status-no-match .paper-route-status-icon { background: #dc2626; }
.paper-route-status-low-confidence .paper-route-status-icon,
.paper-route-status-not-run .paper-route-status-icon,
.paper-route-status-unknown .paper-route-status-icon { background: #64748b; }
.paper-route-status-ambiguous .paper-route-status-icon { background: #ea580c; }

.paper-coverage-route-card-head {
  display: flex;
  align-items: center;
  flex-wrap: wrap;
  gap: 5px;
  min-width: 0;
}

.paper-coverage-route-confidence {
  color: #64748b;
  font-size: 0.66rem;
  font-weight: 720;
}

.paper-coverage-justification-main {
  max-height: 3.9em;
  line-height: 1.3;
}

.paper-coverage-cross-link-list {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
  min-width: 0;
}

.paper-coverage-cross-link-name {
  display: inline;
  min-width: 0;
  max-width: 100%;
  border: 0;
  border-radius: 0;
  background: transparent;
  color: #64748b;
  font-size: 0.72rem;
  font-weight: 400;
  line-height: 1.28;
  padding: 0;
  overflow-wrap: anywhere;
}

.paper-coverage-lean-link {
  border: 0;
  padding: 0;
  background: transparent;
  color: #1d4ed8;
  font: inherit;
  font-size: 0.77rem;
  font-weight: 720;
  text-align: left;
  cursor: pointer;
  overflow: hidden;
  text-overflow: ellipsis;
}

.paper-coverage-lean-link:hover {
  text-decoration: underline;
}

.paper-coverage-row-actions {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 5px;
  margin-top: 2px;
}

.paper-coverage-row-actions button {
  border: 1px solid var(--border);
  background: #ffffff;
  color: #334155;
  padding: 3px 6px;
  font: inherit;
  font-size: 0.66rem;
  font-weight: 700;
  cursor: pointer;
}

.paper-coverage-row-actions button:hover {
  border-color: #93c5fd;
  color: #1d4ed8;
  background: #eff6ff;
}

.paper-coverage-detail {
  grid-column: 1 / -1;
  border-top: 1px solid #fde68a;
  background: #fffbeb;
  padding: 11px 13px 12px 17px;
  display: grid;
  grid-template-columns: minmax(0, 1.2fr) minmax(240px, 0.8fr);
  gap: 10px 14px;
}

.paper-coverage-detail-block {
  min-width: 0;
  background: rgba(255, 255, 255, 0.78);
  border: 1px solid rgba(245, 158, 11, 0.22);
  padding: 8px 9px;
}

.paper-coverage-detail-label {
  margin-bottom: 5px;
  color: #92400e;
  font-size: 0.64rem;
  font-weight: 820;
  text-transform: uppercase;
  letter-spacing: 0.06em;
}

.paper-coverage-detail-text {
  color: #1f2937;
  font-size: 0.78rem;
  line-height: 1.42;
}

.paper-coverage-detail-text p,
.paper-coverage-detail-block p {
  margin: 0 0 0.45em;
}


.paper-coverage-route-chips {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
}

.paper-coverage-route-chip {
  display: inline-flex;
  align-items: center;
  gap: 5px;
  border: 1px solid #e5e7eb;
  background: #ffffff;
  color: #374151;
  padding: 4px 7px;
  font-size: 0.68rem;
}

.paper-coverage-route-chip strong {
  color: #111827;
  font-weight: 750;
}

.paper-coverage-signature {
  margin: 0;
  max-height: 148px;
  overflow: auto;
  color: #0f172a;
  background: #ffffff;
  border: 1px solid #e5e7eb;
  padding: 8px;
  font-size: 0.7rem;
  line-height: 1.35;
  white-space: pre-wrap;
}

.paper-coverage-candidates-block ol {
  margin: 0;
  padding-left: 1.25em;
  color: #334155;
  font-size: 0.72rem;
}

.paper-coverage-candidates-block li + li {
  margin-top: 4px;
}

.paper-coverage-candidates-block span {
  color: #64748b;
  font-size: 0.68rem;
}

.paper-coverage-warning {
  grid-column: 1 / -1;
  color: #991b1b;
  background: #fef2f2;
  border: 1px solid #fecaca;
  padding: 7px 8px;
  font-size: 0.74rem;
}

.paper-coverage-empty {
  padding: 24px;
  color: #64748b;
  text-align: center;
  font-size: 0.82rem;
}

@media (max-width: 1180px) {
  .paper-coverage-summary {
    grid-template-columns: 1fr;
  }
  .paper-coverage-metrics {
    grid-template-columns: repeat(5, minmax(70px, 1fr));
  }
}

@media (max-height: 780px) {
  .paper-coverage-summary p {
    display: none;
  }
  .paper-coverage-summary {
    padding-top: 9px;
    padding-bottom: 8px;
  }
  .paper-coverage-metric {
    padding-top: 5px;
    padding-bottom: 5px;
  }
}

.paper-graph-pane {
  grid-template-rows: auto auto minmax(0, 1fr);
}

.paper-coverage-shell,
.paper-left-empty {
  grid-row: 2 / -1;
}

.paper-graph-canvas {
  grid-row: 3;
}

/* Minimal Formalization Coverage table */
.paper-coverage-shell {
  grid-template-rows: auto minmax(0, 1fr);
  background: #ffffff;
}

.paper-coverage-controls {
  padding: 5px 10px;
  background: #ffffff;
}

.paper-coverage-filter-row {
  gap: 5px;
}

.paper-coverage-filter {
  padding: 3px 7px;
  font-size: 0.7rem;
  background: #ffffff;
}

.paper-coverage-filter.active {
  background: #f3f4f6;
  border-color: #9ca3af;
}

.paper-coverage-search {
  height: 28px;
  background: #ffffff;
  font-size: 0.74rem;
}

.paper-coverage-count {
  font-size: 0.7rem;
}

.paper-coverage-table {
  background: #ffffff;
}

.paper-coverage-table-head,
.paper-coverage-row {
  grid-template-columns: minmax(220px, 0.8fr) minmax(320px, 1.1fr) minmax(340px, 1.15fr);
}

.paper-coverage-table-head {
  padding: 6px 10px;
  background: #f9fafb;
  font-size: 0.62rem;
}

.paper-coverage-rows {
  padding-bottom: 0;
}

.paper-coverage-row {
  min-height: 48px;
  background: #ffffff;
}

.paper-coverage-row:hover {
  background: #fafafa;
}

.paper-coverage-row.selected {
  background: #fffbeb;
  box-shadow: inset 3px 0 0 #d97706;
}

.paper-coverage-cell {
  padding: 7px 9px;
  gap: 3px;
  font-size: 0.72rem;
  line-height: 1.25;
}

.paper-coverage-item-title-row {
  align-items: center;
  gap: 6px;
}

.paper-coverage-item-title-row strong {
  font-size: 0.78rem;
}

.paper-coverage-kind {
  padding: 1px 4px;
  font-size: 0.56rem;
  letter-spacing: 0.035em;
}

.paper-coverage-item-meta {
  display: block;
  color: #6b7280;
  font-size: 0.65rem;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.paper-coverage-status-pill {
  padding: 2px 6px;
  gap: 4px;
  font-size: 0.64rem;
  letter-spacing: 0.02em;
}

.paper-coverage-status-pill span:first-child {
  width: 13px;
  height: 13px;
  font-size: 0.48rem;
}

.paper-coverage-status-blueprint_only span:first-child {
  width: 18px;
  font-size: 0.4rem;
}
.paper-coverage-status-partial span:first-child {
  font-size: 0;
}

.paper-coverage-match-name,
.paper-coverage-justification-main {
  font-size: 0.72rem;
  max-height: none;
  overflow: hidden;
  text-overflow: ellipsis;
}

.paper-coverage-match-name {
  white-space: nowrap;
}

.paper-coverage-justification-main {
  white-space: normal;
  line-height: 1.28;
}

.paper-coverage-muted-line {
  display: inline;
  margin-left: 4px;
  font-size: 0.64rem;
}

.paper-coverage-empty-cell {
  font-size: 0.72rem;
  font-style: normal;
}

/* Semantic area cards: make area purpose/interface more prominent than volume. */
.area-card-meta.compact {
  margin-top: 4px;
  margin-bottom: 4px;
}

.area-semantic-row,
.area-entry-files {
  display: grid;
  grid-template-columns: 72px minmax(0, 1fr);
  gap: 8px;
  align-items: start;
  margin-top: 6px;
  font-size: 0.73rem;
}

.area-semantic-row > span,
.area-entry-files > span {
  color: var(--muted);
  font-weight: 650;
}

.area-semantic-row > div,
.area-entry-files {
  min-width: 0;
}

.area-semantic-row code,
.area-entry-files code {
  display: inline-block;
  max-width: 100%;
  margin: 0 4px 4px 0;
  padding: 1px 5px;
  border: 1px solid var(--border);
  background: var(--surface-subtle);
  color: #1f2937;
  font-size: 0.72rem;
  overflow: hidden;
  text-overflow: ellipsis;
  vertical-align: top;
}

.area-semantic-row.provides code {
  border-color: color-mix(in srgb, var(--area-color, #94a3b8) 45%, var(--border));
  background: color-mix(in srgb, var(--area-color, #94a3b8) 9%, #ffffff);
}

.area-entry-files code {
  white-space: nowrap;
}

.area-why-list {
  margin: 6px 0 0 0;
  padding-left: 16px;
  color: #475569;
  font-size: 0.72rem;
  line-height: 1.32;
}

/* Inline Blueprint reveal inside the Paper tab. */
.paper-html-item:has(.paper-html-blueprint-button) .paper-html-item-main {
  padding-bottom: 7px;
}

.paper-html-item-actions {
  display: flex;
  justify-content: center;
  margin-top: 4px;
  margin-bottom: 0;
  padding-top: 3px;
  border-top: 1px solid #ececec;
}

.paper-html-blueprint-button {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  gap: 4px;
  max-width: min(100%, 420px);
  min-height: 22px;
  border: 1px solid #cbd5e1;
  border-radius: 0;
  background: #fbfdff;
  color: #173a6a;
  font-family: var(--mono);
  font-size: 0.68rem;
  font-weight: 700;
  line-height: 1.1;
  padding: 3px 8px;
  cursor: pointer;
}

.paper-html-blueprint-button:hover,
.paper-html-blueprint-button.active {
  border-color: #2563eb;
  background: #f7fbff;
  color: #1d4ed8;
}

.paper-html-blueprint-button:focus-visible,
.paper-html-blueprint-close:focus-visible {
  outline: 2px solid #2563eb;
  outline-offset: 2px;
}

.paper-html-blueprint-button-icon {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  min-width: 18px;
  height: 14px;
  border: 1px solid currentColor;
  font-size: 0.56rem;
  letter-spacing: 0.02em;
}

.paper-html-blueprint-button-main {
  color: inherit;
}

.paper-html-blueprint-button-separator {
  color: #94a3b8;
  font-weight: 700;
}

.paper-html-blueprint-button-name {
  min-width: 0;
  max-width: 240px;
  overflow: hidden;
  color: #475569;
  font-weight: 650;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.paper-html-blueprint-button.active .paper-html-blueprint-button-name {
  color: #1d4ed8;
}

.paper-html-blueprint-button-meta {
  color: #64748b;
  font-weight: 600;
}

.paper-html-item.blueprint-reveal-target {
  margin-bottom: 1px;
  border-left-width: 6px;
  box-shadow: 0 0 0 1px rgba(37, 99, 235, 0.10);
  z-index: 2;
}

.paper-html-blueprint-reveal {
  position: relative;
  margin: 4px 0 14px;
  padding: 10px 38px 12px 14px;
  border: 1px solid #bfd4f8;
  border-left: 5px solid #2563eb;
  border-radius: 6px;
  background: linear-gradient(180deg, #f8fbff 0%, #ffffff 100%);
  box-shadow: 0 8px 22px rgba(15, 23, 42, 0.08), 0 0 0 1px rgba(37, 99, 235, 0.06);
  color: #172033;
  font-family: Inter, ui-sans-serif, system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
}

.paper-html-blueprint-close {
  position: absolute;
  top: 7px;
  right: 7px;
  width: 26px;
  height: 26px;
  border: 1px solid transparent;
  border-radius: 50%;
  background: rgba(255, 255, 255, 0.72);
  color: #64748b;
  font-size: 1.35rem;
  font-weight: 600;
  line-height: 1;
  cursor: pointer;
}

.paper-html-blueprint-close:hover {
  color: #1d4ed8;
  border-color: #bfdbfe;
  background: #eff6ff;
}

.paper-html-blueprint-grid {
  display: grid;
  gap: 10px;
}

.paper-html-blueprint-card {
  border: 0;
  background: transparent;
  padding: 0;
}

.paper-html-blueprint-card-label {
  margin: 0 0 5px;
  color: #1d4ed8;
  font-family: var(--mono);
  font-size: 0.68rem;
  font-weight: 800;
  letter-spacing: 0.04em;
  line-height: 1.1;
  text-transform: uppercase;
}

.paper-html-blueprint-card .blueprint-latex-block {
  margin-top: 0;
  color: #111827;
  font-family: Georgia, Cambria, "Times New Roman", Times, serif;
  font-size: 0.98rem;
  line-height: 1.48;
}

.paper-html-blueprint-card .blueprint-latex-block p {
  margin: 0 0 0.46em;
  text-align: justify;
}

.paper-html-blueprint-card .blueprint-latex-block p:last-child {
  margin-bottom: 0;
}

.paper-html-blueprint-card .blueprint-display-math {
  overflow-x: auto;
  padding: 5px 0;
}

/* Dual-route Paper → Lean / Paper → Blueprint controls */
.paper-coverage-route-filter-stack {
  display: grid;
  grid-template-columns: minmax(0, 1fr) auto;
  align-items: center;
  gap: 5px 8px;
}

.paper-route-filter-group[data-route-filter-group="lean"] {
  grid-column: 1;
  grid-row: 1;
}

.paper-route-filter-group[data-route-filter-group="blueprint"] {
  grid-column: 1;
  grid-row: 2;
}

.paper-coverage-route-filter-stack > .paper-coverage-count {
  grid-column: 2;
  grid-row: 1 / span 2;
  align-self: center;
}

.paper-route-filter-group {
  display: grid;
  grid-template-columns: auto minmax(0, 1fr);
  align-items: center;
  gap: 6px;
  min-width: 0;
}

.paper-route-filter-label {
  font-size: 10px;
  font-weight: 700;
  color: #475569;
  letter-spacing: 0.035em;
  text-transform: uppercase;
  white-space: nowrap;
}

.paper-route-filter-buttons {
  display: flex;
  flex-wrap: nowrap;
  gap: 4px;
  min-width: 0;
  overflow-x: auto;
  scrollbar-width: thin;
}

.paper-route-filter {
  display: inline-flex;
  align-items: center;
  flex: 0 0 auto;
  gap: 4px;
  border: 1px solid #dbe3ef;
  background: #fff;
  color: #334155;
  font-size: 10px;
  font-weight: 650;
  border-radius: 999px;
  padding: 3px 6px;
  min-height: 22px;
  cursor: pointer;
}

.paper-route-filter:hover {
  border-color: #94a3b8;
  background: #f8fafc;
}

.paper-route-filter.active {
  border-color: #0f172a;
  background: #0f172a;
  color: #fff;
}

.paper-route-filter strong {
  font-size: 9px;
  font-weight: 800;
  min-width: 14px;
  text-align: center;
}

.paper-coverage-filter-row-secondary {
  justify-content: flex-end;
  margin-top: 0;
}

.paper-coverage-route-cell {
  display: grid;
  gap: 4px;
  min-width: 0;
}

.paper-route-status {
  display: inline-flex;
  width: fit-content;
  max-width: 100%;
  align-items: center;
  border-radius: 999px;
  border: 1px solid #dbe3ef;
  background: #f8fafc;
  color: #475569;
  padding: 2px 7px;
  font-size: 10px;
  font-weight: 750;
  letter-spacing: 0.01em;
  white-space: normal;
  overflow-wrap: anywhere;
}

.paper-route-status-exact {
  color: #166534;
  background: #f0fdf4;
  border-color: #bbf7d0;
}

.paper-route-status-partial {
  color: #92400e;
  background: #fffbeb;
  border-color: #fde68a;
}

.paper-route-status-related {
  color: #1d4ed8;
  background: #eff6ff;
  border-color: #bfdbfe;
}

.paper-route-status-no-match,
.paper-route-status-low-confidence,
.paper-route-status-not-run,
.paper-route-status-unknown {
  color: #64748b;
  background: #f8fafc;
  border-color: #e2e8f0;
}

.paper-route-status-ambiguous {
  color: #7c2d12;
  background: #fff7ed;
  border-color: #fed7aa;
}

.paper-coverage-route-substatus {
  color: #64748b;
  font-size: 11px;
  line-height: 1.35;
}

.paper-coverage-link-resolved {
  color: #166534;
}

.paper-coverage-link-unresolved {
  color: #b45309;
}

.paper-coverage-link-no-link,
.paper-coverage-link-no-match {
  color: #64748b;
}

.paper-coverage-mini-action {
  width: fit-content;
  border: 1px solid #dbe3ef;
  background: #fff;
  color: #0f172a;
  border-radius: 999px;
  padding: 3px 8px;
  font-size: 10px;
  font-weight: 750;
  cursor: pointer;
}

.paper-coverage-mini-action:hover {
  border-color: #94a3b8;
  background: #f8fafc;
}

.paper-match-routes {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
  gap: 10px;
  margin-top: 12px;
}

.paper-match-route-card {
  border: 1px solid #e2e8f0;
  background: #fff;
  border-radius: 12px;
  padding: 10px;
  display: grid;
  gap: 7px;
  min-width: 0;
}

.paper-match-route-head {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 8px;
}

.paper-match-route-title {
  font-size: 11px;
  font-weight: 800;
  color: #334155;
  letter-spacing: 0.04em;
  text-transform: uppercase;
}

.paper-match-route-value {
  min-height: 20px;
  font-size: 12px;
  color: #0f172a;
  overflow-wrap: anywhere;
}

.paper-match-route-value code {
  font-size: 11px;
}

.paper-match-route-substatus {
  color: #64748b;
  font-size: 11px;
  line-height: 1.35;
}

.paper-match-route-rationale {
  color: #475569;
  font-size: 11px;
  line-height: 1.35;
}

.paper-match-route-action {
  width: fit-content;
  margin-top: 2px;
}

.paper-match-grid-single {
  grid-template-columns: 1fr;
}

@media (max-width: 900px) {
  .paper-coverage-route-filter-stack {
    grid-template-columns: minmax(0, 1fr);
  }
  .paper-route-filter-group {
    grid-template-columns: auto minmax(0, 1fr);
  }
  .paper-route-filter-group[data-route-filter-group="blueprint"] {
    grid-column: 1;
    grid-row: 2;
  }
  .paper-coverage-route-filter-stack > .paper-coverage-count {
    grid-column: 1;
    grid-row: 3;
    justify-self: end;
  }
  .paper-match-routes {
    grid-template-columns: 1fr;
  }
}

/* Route-aware status/filter refinements */
.paper-coverage-status-formalized_via_blueprint { border-color: rgba(21, 128, 61, 0.28); color: #166534; background: #f0fdf4; }
.paper-coverage-status-formalized_via_blueprint span:first-child { background: #15803d; width: 20px; font-size: 0.42rem; }
.paper-coverage-status-statement_only_via_blueprint { border-color: rgba(101, 163, 13, 0.28); color: #3f6212; background: #f7fee7; }
.paper-coverage-status-statement_only_via_blueprint span:first-child { background: #65a30d; width: 20px; font-size: 0.42rem; }
.paper-coverage-status-partial_via_blueprint { border-color: rgba(217, 119, 6, 0.28); color: #92400e; background: #fffbeb; }
.paper-coverage-status-partial_via_blueprint span:first-child { background: #d97706; width: 20px; font-size: 0.42rem; }
.paper-coverage-status-blueprint_planned,
.paper-coverage-status-blueprint_link_unresolved { border-color: rgba(37, 99, 235, 0.28); color: #1d4ed8; background: #eff6ff; }
.paper-coverage-status-blueprint_planned span:first-child,
.paper-coverage-status-blueprint_link_unresolved span:first-child { background: #2563eb; width: 20px; font-size: 0.42rem; }
.paper-coverage-status-conflict_needs_review { border-color: rgba(220, 38, 38, 0.24); color: #991b1b; background: #fef2f2; }
.paper-coverage-status-conflict_needs_review span:first-child { background: #dc2626; }

.paper-coverage-filter-conflict_needs_review .paper-coverage-filter-icon { background: #dc2626; }
.paper-coverage-filter-unknown .paper-coverage-filter-icon { background: #64748b; }
.paper-coverage-filter-conflict_needs_review.active { border-color: rgba(220, 38, 38, 0.30); background: #fef2f2; }
.paper-coverage-filter-unknown.active { border-color: rgba(100, 116, 139, 0.30); background: #f8fafc; }

.paper-route-filter.active {
  color: #0f172a;
  border-color: #94a3b8;
  background: #f1f5f9;
}
.paper-route-filter.paper-coverage-filter-formalized.active {
  border-color: rgba(21, 128, 61, 0.34);
  background: #f0fdf4;
}
.paper-route-filter.paper-coverage-filter-statement_only.active {
  border-color: rgba(101, 163, 13, 0.34);
  background: #f7fee7;
}
.paper-route-filter.paper-coverage-filter-partial.active {
  border-color: rgba(217, 119, 6, 0.34);
  background: #fffbeb;
}
.paper-route-filter.paper-coverage-filter-blueprint_only.active {
  border-color: rgba(37, 99, 235, 0.34);
  background: #eff6ff;
}
.paper-route-filter.paper-coverage-filter-not_locally_formalized.active,
.paper-route-filter.paper-coverage-filter-conflict_needs_review.active {
  border-color: rgba(220, 38, 38, 0.30);
  background: #fef2f2;
}
.paper-route-filter.disabled {
  opacity: 0.55;
}

.paper-coverage-status-routes {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
  margin-top: 2px;
}
.paper-coverage-route-mini {
  display: inline-flex;
  align-items: center;
  gap: 4px;
  width: fit-content;
  border: 1px solid #dbe3ef;
  background: #f8fafc;
  color: #475569;
  padding: 2px 5px;
  font-size: 0.61rem;
  font-weight: 730;
  line-height: 1.15;
  text-transform: none;
  letter-spacing: 0;
}
.paper-coverage-route-mini strong {
  font-size: 0.55rem;
  color: inherit;
  opacity: 0.75;
  text-transform: uppercase;
  letter-spacing: 0.035em;
}
.paper-coverage-route-mini.paper-route-status-exact {
  color: #166534;
  background: #f0fdf4;
  border-color: #bbf7d0;
}
.paper-coverage-route-mini.paper-route-status-partial {
  color: #92400e;
  background: #fffbeb;
  border-color: #fde68a;
}
.paper-coverage-route-mini.paper-route-status-related {
  color: #1d4ed8;
  background: #eff6ff;
  border-color: #bfdbfe;
}
.paper-coverage-route-mini.paper-route-status-no-match,
.paper-coverage-route-mini.paper-route-status-low-confidence,
.paper-coverage-route-mini.paper-route-status-not-run,
.paper-coverage-route-mini.paper-route-status-unknown {
  color: #64748b;
  background: #f8fafc;
  border-color: #e2e8f0;
}
.paper-coverage-route-mini.paper-route-status-ambiguous {
  color: #7c2d12;
  background: #fff7ed;
  border-color: #fed7aa;
}

.paper-html-blueprint-button-status {
  font-weight: 850;
}
.paper-html-blueprint-button .paper-html-blueprint-button-name {
  color: #64748b;
  font-weight: 650;
  max-width: 120px;
}
.paper-html-blueprint-button .paper-html-blueprint-button-name::before {
  content: "(";
}
.paper-html-blueprint-button .paper-html-blueprint-button-name::after {
  content: ")";
}

.paper-route-assessment-stack {
  display: grid;
  gap: 14px;
  min-width: 0;
  max-width: 100%;
}

.paper-route-assessment {
  min-width: 0;
  max-width: 100%;
  padding-top: 4px;
  padding-bottom: 8px;
  border-bottom: 1px solid rgba(226, 232, 240, 0.9);
}

.paper-route-assessment:last-child {
  border-bottom: 0;
}

.paper-route-assessment-heading {
  align-items: flex-start;
  flex-wrap: wrap;
}

.paper-route-assessment-badges {
  display: flex;
  min-width: 0;
  max-width: 100%;
  align-items: center;
  justify-content: flex-start;
  gap: 6px;
  flex-wrap: wrap;
}

.paper-route-target {
  display: grid;
  min-width: 0;
  max-width: 100%;
  gap: 2px;
  margin-top: 5px;
  padding: 6px 8px;
  border: 1px solid rgba(226, 232, 240, 0.9);
  border-radius: 8px;
  background: #f8fafc;
}

.paper-route-target-label {
  color: var(--muted);
  font-size: 0.62rem;
  font-weight: 800;
  letter-spacing: 0.045em;
  text-transform: uppercase;
}

.paper-route-target-name {
  color: var(--text);
  font-size: 0.74rem;
  line-height: 1.25;
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
}
.paper-route-target-name code {
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
}

.paper-route-target-substatus,
.paper-route-no-candidates {
  color: var(--muted);
  font-size: 0.68rem;
  line-height: 1.25;
}


/* Keep paper match details inside the selection/code panes. Long theorem names,
   Lean declarations and LLM rationales should wrap instead of extending under
   the Lean code panel. */
.paper-focus-block,
.paper-match-card,
.paper-match-card-header,
.paper-match-title-block,
.paper-llm-assessment,
.paper-candidates,
.paper-candidate-list,
.paper-candidate-row,
.paper-candidate-main,
.paper-match-routes,
.paper-match-route-card,
.paper-route-target,
.paper-route-assessment-stack {
  min-width: 0;
  max-width: 100%;
}

.paper-match-title,
.paper-match-subtitle,
.paper-match-value,
.paper-match-value code,
.paper-llm-rationale,
.paper-llm-judgment,
.paper-match-route-value,
.paper-match-route-value code,
.paper-match-route-substatus,
.paper-match-route-rationale,
.paper-route-target-substatus,
.paper-route-no-candidates,
.paper-candidates > summary {
  white-space: normal;
  overflow-wrap: anywhere;
  word-break: break-word;
}

.paper-candidate-row {
  align-items: start;
}


/* Formalization coverage: keep the table inside its pane.
   The previous grid used fixed minimums that could exceed the available width,
   so the Lean column was clipped by the code panel. These overrides make all
   columns shrinkable and force long names/rationales to wrap vertically. */
.paper-coverage-table,
.paper-coverage-table-head,
.paper-coverage-rows,
.paper-coverage-row,
.paper-coverage-cell,
.paper-coverage-route-card,
.paper-coverage-route-cell,
.paper-coverage-route-status-line,
.paper-coverage-route-item,
.paper-coverage-route-reason,
.paper-coverage-route-link,
.paper-coverage-route-secondary,
.paper-route-status,
.paper-coverage-status-pill,
.paper-coverage-match-name,
.paper-coverage-justification-main,
.paper-coverage-cross-link-list,
.paper-coverage-cross-link-name,
.paper-coverage-muted-line,
.paper-coverage-item-title-row,
.paper-coverage-item-title-row strong,
.paper-coverage-item-meta {
  min-width: 0;
  max-width: 100%;
}

.paper-coverage-table-head,
.paper-coverage-row {
  grid-template-columns: minmax(128px, 0.72fr) minmax(0, 1fr) minmax(0, 1fr) !important;
}

.paper-coverage-table-head {
  overflow: hidden;
}

.paper-coverage-table-head span {
  min-width: 0;
  overflow-wrap: anywhere;
}

.paper-coverage-cell {
  overflow: hidden;
}

.paper-coverage-route-label {
  flex: 0 0 64px;
}

.paper-coverage-route-status-line,
.paper-coverage-route-item,
.paper-coverage-route-reason,
.paper-coverage-route-link,
.paper-coverage-route-secondary {
  display: grid;
  grid-template-columns: 64px minmax(0, 1fr);
  column-gap: 6px;
  align-items: center;
}

.paper-coverage-route-reason {
  align-items: center;
}

.paper-route-status,
.paper-coverage-status-pill {
  width: fit-content;
  max-width: 100%;
  white-space: normal;
  overflow-wrap: anywhere;
}

.paper-coverage-item-title-row strong,
.paper-coverage-item-meta,
.paper-coverage-match-name,
.paper-coverage-justification-main,
.paper-coverage-cross-link-name,
.paper-coverage-muted-line,
.paper-coverage-lean-link {
  white-space: normal !important;
  overflow: visible !important;
  text-overflow: clip !important;
  overflow-wrap: anywhere;
  word-break: break-word;
}

.paper-coverage-justification-main {
  max-height: none !important;
}

.paper-coverage-muted-line {
  display: block;
  margin-left: 0;
}

@media (max-width: 760px) {
  .paper-coverage-table-head,
  .paper-coverage-row {
    grid-template-columns: minmax(108px, 0.62fr) minmax(0, 1fr) minmax(0, 1fr) !important;
  }

  .paper-coverage-cell {
    padding-left: 6px;
    padding-right: 6px;
  }

  .paper-coverage-route-label {
    flex-basis: 58px;
    font-size: 0.54rem;
  }

  .paper-coverage-route-status-line,
  .paper-coverage-route-item,
  .paper-coverage-route-reason,
  .paper-coverage-route-link,
  .paper-coverage-route-secondary {
    grid-template-columns: 58px minmax(0, 1fr);
  }
}