/* Verso Literate CSS */

:root {
    /* Font families */
    --verso-code-font-family: "Monaco", "Menlo", "Ubuntu Mono", monospace;
    --verso-text-font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif;
    --verso-structure-font-family:
        -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif;

    /* Colors */
    --verso-text-color: #333;
    --verso-structure-color: #333;
    --verso-background-color: #ffffff;
    --verso-surface-color: #f8f9fa;
    --verso-border-color: #e9ecef;
    --verso-link-color: #0066cc;
    --verso-link-visited-color: #551a8b;
    --verso-link-hover-bg: #e3f2fd;
    --verso-muted-color: #6c757d;
    --verso-current-bg: #0066cc;
    --verso-current-fg: white;
    --verso-breadcrumb-color: #495057;

    /* Code boxes */
    --verso-code-box-background-color: #f6f8fa;
    --verso-code-box-border-color: #e1e4e8;

    /* Prose */
    --verso-prose-max-width: 65ch;
    --verso-blockquote-border-color: #dfe2e5;
    --verso-blockquote-color: #6a737d;
    --verso-inline-code-bg: #f0f2f4;
    --verso-docstring-border-color: #ddd;

    /* Imports */
    --verso-imports-summary-color: #586069;

    /* Output */
    --verso-output-color: #555;

    /* Copy button */
    --verso-copy-button-bg: #e9ecef;
    --verso-copy-button-border: #d1d5db;
    --verso-copy-button-color: #586069;
    --verso-copy-button-hover-bg: #d1d5db;
    --verso-copy-button-copied-color: #22863a;

    /* Hamburger */
    --verso-hamburger-bg: #fff;
    --verso-hamburger-border: #dee2e6;
    --verso-hamburger-bar-color: #333;

    /* Diagnostic colors */
    --verso-warning-color: #fff3cd;
    --verso-error-color: #cc0000;
    --verso-warning-indicator-color: #b8860b;
    --verso-error-indicator-color: #dc3545;
    --verso-info-indicator-color: #0066cc;

    /* Syntax highlighting weight/style */
    --verso-code-keyword-weight: bold;
    --verso-code-keyword-style: normal;
}

/* Dark mode defaults */
@media (prefers-color-scheme: dark) {
    :root {
        --verso-text-color: #e0e0e0;
        --verso-structure-color: #e0e0e0;
        --verso-background-color: #1a1a2e;
        --verso-surface-color: #16213e;
        --verso-border-color: #2a2a4a;
        --verso-link-color: #90caf9;
        --verso-link-visited-color: #ce93d8;
        --verso-link-hover-bg: #1a2744;
        --verso-muted-color: #9e9e9e;
        --verso-current-bg: #1565c0;
        --verso-current-fg: white;
        --verso-breadcrumb-color: #bdbdbd;
        --verso-code-box-background-color: #0f1525;
        --verso-code-box-border-color: #2a2a4a;
        --verso-blockquote-border-color: #3a3a5a;
        --verso-blockquote-color: #9e9e9e;
        --verso-inline-code-bg: #1a1a2e;
        --verso-docstring-border-color: #3a3a5a;
        --verso-imports-summary-color: #9e9e9e;
        --verso-output-color: #bdbdbd;
        --verso-copy-button-bg: #2a2a4a;
        --verso-copy-button-border: #3a3a5a;
        --verso-copy-button-color: #9e9e9e;
        --verso-copy-button-hover-bg: #3a3a5a;
        --verso-copy-button-copied-color: #66bb6a;
        --verso-hamburger-bg: #16213e;
        --verso-hamburger-border: #2a2a4a;
        --verso-hamburger-bar-color: #e0e0e0;
        --verso-warning-color: #3d3000;
        --verso-error-color: #ff6b6b;
        --verso-warning-indicator-color: #ffc107;
        --verso-error-indicator-color: #ff6b6b;
        --verso-info-indicator-color: #64b5f6;
        --verso-selected-color: #1a2744;
    }

    /* Hover tooltips (tippy) */
    .tippy-box[data-theme~="lean"],
    .tippy-box[data-theme~="error"],
    .tippy-box[data-theme~="warning"],
    .tippy-box[data-theme~="info"] {
        background-color: #2a2a4a;
        color: #e0e0e0;
        border-color: #4a4a6a;
    }
    .tippy-box[data-theme~="lean"] > .tippy-arrow::before,
    .tippy-box[data-theme~="error"] > .tippy-arrow::before,
    .tippy-box[data-theme~="warning"] > .tippy-arrow::before,
    .tippy-box[data-theme~="info"] > .tippy-arrow::before {
        border-color: #2a2a4a;
    }
    .tippy-box[data-theme~="tactic"] {
        background-color: #2a2a4a;
        color: #e0e0e0;
        border-color: #4a4a6a;
    }
    .tippy-box[data-theme~="tactic"] > .tippy-arrow::before {
        border-color: #2a2a4a;
    }
    .tippy-box[data-theme~="message"] > .tippy-arrow::before {
        border-color: #2a2a4a;
    }

    /* Binding highlight on hover */
    .hl.lean .token.binding-hl,
    .hl.lean .literal.string:hover,
    .hl.lean .token.typed:hover {
        background-color: #3a3a5a;
    }

    /* Tactic/proof state hover */
    .hl.lean .tactic:has(.tactic-toggle:not(:checked)) > label:hover {
        background-color: #3a3a5a;
    }

    /* Popup content inside tooltips */
    .hl.lean.popup {
        background-color: #2a2a4a;
        color: #e0e0e0;
    }
    .hl.lean .hover-info {
        color: #e0e0e0;
    }
    .hl.lean .hover-info code {
        color: #e0e0e0;
    }
    .hl.lean .hover-info .sep {
        border-top-color: #4a4a6a;
    }

    /* Diagnostic message backgrounds */
    .hl.lean .hover-info.messages > code.error,
    .hl.lean .hover-info.messages > code.warning,
    .hl.lean .hover-info.messages > code.information {
        background-color: #1a1a2e;
    }

    /* Tactic state */
    .hl.lean .tactic-state,
    .hl.lean.popup .tactic-state {
        background-color: #2a2a4a;
        color: #e0e0e0;
        border-color: #4a4a6a;
    }
}

/* Reset and base styles */
* {
    margin: 0;
    padding: 0;
    box-sizing: border-box;
}

body {
    font-family: var(--verso-text-font-family);
    line-height: 1.6;
    color: var(--verso-text-color);
    background: var(--verso-background-color);
    height: 100vh;
    height: 100dvh;
    overflow: hidden;
}

/* Accessibility: focus indicators */
a:focus-visible,
button:focus-visible,
summary:focus-visible,
input:focus-visible,
[tabindex]:focus-visible {
    outline: 2px solid var(--verso-link-color);
    outline-offset: 2px;
}

/* Accessibility: reduced motion */
@media (prefers-reduced-motion: reduce) {
    *,
    *::before,
    *::after {
        animation-duration: 0.01ms !important;
        transition-duration: 0.01ms !important;
    }
}

/* Skip-to-content link for accessibility */
.skip-link {
    position: absolute;
    top: -40px;
    left: 0;
    background: var(--verso-link-color);
    color: var(--verso-current-fg);
    padding: 0.5rem 1rem;
    z-index: 2000;
    transition: top 0.2s ease;
}

.skip-link:focus {
    top: 0;
}

/* Layout container */
.layout {
    display: flex;
    height: 100vh;
    height: 100dvh;
}

/* Sidebar */
.sidebar {
    width: 300px;
    background: var(--verso-surface-color);
    border-right: 1px solid var(--verso-border-color);
    overflow-y: auto;
    flex-shrink: 0;
}

.sidebar-content {
    padding: 1rem;
}

/* Mobile-specific sidebar content spacing */
@media (max-width: 768px) {
    .sidebar-content {
        padding-top: 4rem;
    }
}

/* Module tree styling */
.module-tree {
    font-family: var(--verso-code-font-family);
    font-size: 0.875rem;
}

.module-tree details {
    margin-left: 1rem;
}

.module-tree summary {
    cursor: pointer;
    padding: 0.25rem 0.5rem;
    border-radius: 0.25rem;
    list-style: none;
    position: relative;
    transition: background-color 0.2s ease;
}

.module-tree summary::-webkit-details-marker {
    display: none;
}

.module-tree summary:hover {
    background-color: var(--verso-border-color);
}

.module-tree summary a {
    color: var(--verso-link-color);
    text-decoration: none;
}

.module-tree summary a:hover {
    text-decoration: underline;
}

.module-tree summary.current {
    background-color: var(--verso-current-bg);
    color: var(--verso-current-fg);
}

.module-tree summary.current a {
    color: var(--verso-current-fg);
}

.module-tree summary::before {
    content: "\25B6";
    position: absolute;
    left: -0.75rem;
    transition: transform 0.2s ease;
    font-size: 0.75rem;
    color: var(--verso-muted-color);
}

.module-tree details[open] > summary::before {
    transform: rotate(90deg);
}

.module-tree .leaf {
    margin-left: 1rem;
    padding: 0.25rem 0.5rem;
    border-radius: 0.25rem;
}

.module-tree .leaf a {
    color: var(--verso-link-color);
    text-decoration: none;
}

.module-tree .leaf a:hover {
    text-decoration: underline;
}

.module-tree .current {
    background-color: var(--verso-current-bg);
    color: var(--verso-current-fg);
}

.module-tree .current a {
    color: var(--verso-current-fg);
}

/* Single-root nav: no indent for top-level children */
.module-tree > .leaf,
.module-tree > details {
    margin-left: 0;
}

/* Single-root nav title */
.module-tree .nav-title {
    font-weight: bold;
    padding: 0.25rem 0.5rem;
    margin-bottom: 0.25rem;
    font-size: 1rem;
    color: var(--verso-structure-color);
}

.module-tree .nav-title a {
    color: var(--verso-structure-color);
    text-decoration: none;
}

.module-tree .nav-title a:hover {
    text-decoration: underline;
}

.module-tree .custom-title {
    font-family: var(--verso-structure-font-family);
}

/* Main content area */
.main-area {
    flex: 1;
    display: flex;
    flex-direction: column;
    overflow: hidden;
}

/* Title bar */
.title-bar {
    background: var(--verso-background-color);
    border-bottom: 1px solid var(--verso-border-color);
    padding: 1rem 1.5rem;
    flex-shrink: 0;
    position: relative;
}

.breadcrumbs {
    list-style: none;
    display: flex;
    flex-wrap: wrap;
    align-items: center;
    font-size: 0.9rem;
    font-family: var(--verso-code-font-family);
}

.breadcrumbs li {
    display: flex;
    align-items: center;
}

.breadcrumbs li:not(:last-child)::after {
    content: "\00B7";
    margin: 0;
    color: var(--verso-muted-color);
    font-weight: bold;
}

.breadcrumbs a {
    color: var(--verso-link-color);
    text-decoration: none;
    padding: 0.25rem 0.5rem;
    border-radius: 0.25rem;
    transition: background-color 0.2s ease;
}

.breadcrumbs a:hover {
    background-color: var(--verso-link-hover-bg);
    text-decoration: underline;
}

.breadcrumbs .current {
    font-weight: 600;
    color: var(--verso-breadcrumb-color);
    padding: 0.25rem 0.5rem;
    border-radius: 0.25rem;
}

/* Content wrapper: flex row for code content + page ToC */
.content-wrapper {
    flex: 1;
    display: flex;
    flex-direction: row;
    overflow: hidden;
}

/* Links */
a {
    color: var(--verso-link-color);
}

a:visited {
    color: var(--verso-link-visited-color);
}

/* Code content area */
.code-content {
    flex: 1;
    overflow-y: auto;
    padding: 2rem;
    background: var(--verso-background-color);
}

/* Page table of contents (right sidebar) */
.page-toc {
    width: 220px;
    flex-shrink: 0;
    overflow-y: auto;
    padding: 1.5rem 1rem;
    border-left: 1px solid var(--verso-border-color);
    font-size: 0.8125rem;
    line-height: 1.5;
}

.page-toc-title {
    font-weight: 600;
    font-size: 0.75rem;
    text-transform: uppercase;
    letter-spacing: 0.05em;
    color: var(--verso-muted-color);
    margin-bottom: 0.75rem;
}

.page-toc ul {
    list-style: none;
    padding-left: 0;
}

.page-toc li {
    padding: 0.15rem 0;
}

.page-toc li.toc-level-2 {
    padding-left: 0.75rem;
}

.page-toc li.toc-level-3 {
    padding-left: 1.5rem;
}

.page-toc a {
    color: var(--verso-muted-color);
    text-decoration: none;
    transition: color 0.15s ease;
}

.page-toc a:hover {
    color: var(--verso-link-color);
}

@media (max-width: 1024px) {
    .page-toc {
        display: none;
    }
}

/* Code boxes: contain highlighted code, markdown docstrings, verso docstrings */
.code-box {
    background: var(--verso-code-box-background-color);
    border: 1px solid var(--verso-code-box-border-color);
    border-radius: 0.5rem;
    padding: 1rem 1.5rem;
    margin-bottom: 1.5rem;
    font-family: var(--verso-code-font-family);
    font-size: 0.95rem;
    line-height: 1.5;
    overflow-x: auto;
    position: relative;
}

/* Highlight the target definition when navigating via #id */
.hl.lean .token:target {
    background-color: var(--verso-selected-color, #def);
    outline: auto;
    scroll-margin-top: 4rem;
}

/* Prose (module docstrings) flowing between code boxes */
.code-content > .verso-text.mod-doc,
.code-content > .md-text.mod-doc {
    max-width: var(--verso-prose-max-width);
    margin-bottom: 1.5rem;
    font-family: var(--verso-text-font-family);
    font-size: 1rem;
    line-height: 1.7;
}

.code-content > .verso-text.mod-doc > *,
.code-content > .md-text.mod-doc > * {
    margin-bottom: 0.75rem;
    display: block;
}

.code-content > .verso-text.mod-doc > *:last-child,
.code-content > .md-text.mod-doc > *:last-child {
    margin-bottom: 0;
}

.code-content > .verso-text.mod-doc h1,
.code-content > .md-text.mod-doc h1 {
    font-size: 1.75rem;
    margin-top: 1.5rem;
    margin-bottom: 0.75rem;
    border-bottom: 1px solid var(--verso-border-color);
    padding-bottom: 0.5rem;
}

.code-content > .verso-text.mod-doc h2,
.code-content > .md-text.mod-doc h2 {
    font-size: 1.5rem;
    margin-top: 1.25rem;
    margin-bottom: 0.5rem;
}

.code-content > .verso-text.mod-doc h3,
.code-content > .md-text.mod-doc h3 {
    font-size: 1.25rem;
    margin-top: 1rem;
    margin-bottom: 0.5rem;
}

.code-content > .verso-text.mod-doc ul,
.code-content > .md-text.mod-doc ul {
    padding-left: 1.5em;
}

.code-content > .verso-text.mod-doc ol,
.code-content > .md-text.mod-doc ol {
    padding-left: 1.5em;
}

.code-content > .verso-text.mod-doc li,
.code-content > .md-text.mod-doc li {
    margin-bottom: 0.25rem;
}

.code-content > .verso-text.mod-doc blockquote,
.code-content > .md-text.mod-doc blockquote {
    border-left: 4px solid var(--verso-blockquote-border-color);
    padding: 0.25rem 1rem;
    color: var(--verso-blockquote-color);
    margin: 0.5rem 0;
}

.code-content > .verso-text.mod-doc code,
.code-content > .md-text.mod-doc code {
    background: var(--verso-inline-code-bg);
    padding: 0.15rem 0.3rem;
    border-radius: 0.2rem;
    font-family: var(--verso-code-font-family);
    font-size: 0.9em;
}

.code-content > .verso-text.mod-doc pre,
.code-content > .md-text.mod-doc pre {
    background: var(--verso-code-box-background-color);
    padding: 0.75rem 1rem;
    border-radius: 0.375rem;
    overflow-x: auto;
    font-family: var(--verso-code-font-family);
    font-size: 0.9em;
}

/* Docstrings within code boxes (non-modDoc) */
.code-box .verso-text,
.code-box .md-text {
    margin-left: calc(var(--indent, 0) * 1ch);
    max-width: 40em;
    width: max-content;
}

.code-box .verso-text::before,
.code-box .md-text::before {
    content: "/--";
    display: block;
    width: min-content;
}

.code-box .verso-text.mod-doc::before,
.code-box .md-text.mod-doc::before {
    content: "/-!";
    display: block;
    width: min-content;
}

.code-box .verso-text::after,
.code-box .md-text::after {
    content: "-/";
    display: block;
    width: min-content;
}

.code-box .verso-text > *,
.code-box .md-text > * {
    width: max-content;
    max-width: 100%;
    font-family: var(--verso-text-font-family);
    margin-bottom: 0.5rem;
    display: block;
}

.code-box .verso-text > *:last-child,
.code-box .md-text > *:last-child {
    margin-bottom: 0;
}

.code-box .verso-text ul,
.code-box .md-text ul {
    padding-left: 1.5em;
}

.code-box .verso-text ul > li,
.code-box .md-text ul > li {
    margin-bottom: 0.5rem;
}

.code-box .verso-text ul > li:last-child,
.code-box .md-text ul > li:last-child {
    margin-bottom: 0;
}

.code-box .verso-text dt,
.code-box .md-text dt {
    padding-left: 0.5em;
    font-weight: bold;
}

.code-box .verso-text dd,
.code-box .md-text dd {
    padding-left: 1.5em;
}

.code-box .verso-text dd:not(:last-child),
.code-box .md-text dd:not(:last-child) {
    margin-bottom: 0.5rem;
}

.code-box .verso-text pre,
.code-box .md-text pre {
    font-family: var(--verso-code-font-family, monospace);
}

/* Imports list (collapsible, collapsed by default) */
.imports-list {
    margin-bottom: 1.5rem;
    border: 1px solid var(--verso-code-box-border-color);
    border-radius: 0.375rem;
    background: var(--verso-code-box-background-color, var(--verso-surface-color));
}

.imports-list summary {
    cursor: pointer;
    font-weight: 600;
    font-size: 0.9rem;
    color: var(--verso-imports-summary-color);
    padding: 0.5rem 1rem;
}

.imports-list .imports-code {
    padding: 0 var(--verso--box-padding, 1rem) var(--verso--box-padding, 1rem);
}

/* Command output blocks */
.code-box .lean-output {
    border-top: 1px solid var(--verso-code-box-border-color);
    padding: 0.5em 1em;
    font-family: var(--verso-code-font-family, monospace);
    white-space: pre-wrap;
    color: var(--verso-output-color);
}

/* Copy button */
.copy-button {
    position: absolute;
    top: 0.5rem;
    right: 0.5rem;
    background: var(--verso-copy-button-bg);
    border: 1px solid var(--verso-copy-button-border);
    border-radius: 0.25rem;
    padding: 0.25rem 0.5rem;
    cursor: pointer;
    font-size: 0.75rem;
    color: var(--verso-copy-button-color);
    opacity: 0;
    transition: opacity 0.2s ease;
}

.code-box:hover .copy-button {
    opacity: 1;
}

.copy-button:hover {
    background: var(--verso-copy-button-hover-bg);
}

.copy-button.copied {
    color: var(--verso-copy-button-copied-color);
}

/* Landing page */
.landing-page {
    max-width: 800px;
    margin: 0 auto;
    padding: 2rem;
}

.landing-page h1 {
    font-size: 2rem;
    margin-bottom: 1.5rem;
    border-bottom: 2px solid var(--verso-border-color);
    padding-bottom: 0.75rem;
}

.module-toc {
    list-style: none;
    padding-left: 0;
}

.module-toc .module-toc {
    padding-left: 1.5rem;
}

.module-toc li {
    padding: 0.25rem 0;
}

.module-toc a {
    color: var(--verso-link-color);
    text-decoration: none;
    font-family: var(--verso-code-font-family);
}

.module-toc a:hover {
    text-decoration: underline;
}

/* Hamburger menu (hidden by default) */
.menu-toggle {
    display: none;
}

.hamburger {
    display: none;
    position: fixed;
    top: 1rem;
    left: 1rem;
    z-index: 1001;
    background: var(--verso-hamburger-bg);
    border: 1px solid var(--verso-hamburger-border);
    border-radius: 0.375rem;
    padding: 0.5rem;
    cursor: pointer;
    box-shadow: 0 2px 4px rgba(0, 0, 0, 0.1);
}

.hamburger span {
    display: block;
    width: 20px;
    height: 2px;
    background: var(--verso-hamburger-bar-color);
    margin: 4px 0;
    transition: 0.3s;
}

/* Mobile styles */
@media (max-width: 768px) {
    .hamburger {
        display: block;
    }

    .sidebar {
        position: fixed;
        top: 0;
        left: -300px;
        height: 100vh;
        z-index: 1000;
        transition: left 0.3s ease;
        box-shadow: 2px 0 10px rgba(0, 0, 0, 0.1);
    }

    .menu-toggle:checked + .hamburger + .layout .sidebar {
        left: 0;
    }

    .menu-toggle:checked + .hamburger span:nth-child(1) {
        transform: translate(0px, 6px) rotate(45deg);
    }

    .menu-toggle:checked + .hamburger span:nth-child(2) {
        opacity: 0;
    }

    .menu-toggle:checked + .hamburger span:nth-child(3) {
        transform: translate(0px, -6px) rotate(-45deg);
    }

    .main-area {
        width: 100%;
    }

    .title-bar {
        padding-left: 4rem;
    }

    /* Overlay when menu is open */
    .menu-toggle:checked + .hamburger + .layout::after {
        content: "";
        position: fixed;
        top: 0;
        left: 0;
        right: 0;
        bottom: 0;
        background: rgba(0, 0, 0, 0.5);
        z-index: 999;
    }
}