:root {
    /** Typography **/
    /*
    Three offline font-role stacks (system fonts only, no web/CDN fonts):
      - display: confident sans for titles and headings
      - prose:   serif for informal mathematical prose (harmonizes with KaTeX)
      - mono-ui: UI monospace for the "apparatus" (captions/badges/labels)
    */
    --font-display: ui-sans-serif, system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, sans-serif;
    --font-prose: "Charter", "Bitstream Charter", "Iowan Old Style", "Palatino Linotype", Palatino, Georgia, "Times New Roman", serif;
    --font-mono-ui: ui-monospace, "SF Mono", "JetBrains Mono", Menlo, Consolas, "Liberation Mono", monospace;

    /* The font family used for headers, ToC entries, etc */
    --verso-structure-font-family: var(--font-display);
    /* The font family used for body text */
    --verso-text-font-family: var(--font-display);
    /* The font family used for code */
    --verso-code-font-family: monospace;

    /** Text colors **/
    --verso-text-color: #15212b;
    --verso-code-color: #15212b;
    --verso-structure-color: #15212b;
    /* Page background (consumed by the `body` rule in book.css). Cool light canvas by default. */
    --verso-background-color: #f4f6f8;

    /** Selected items (e.g. search results) */
    --verso-selected-color: #e1ecf9;

    /** UI surfaces, borders, links, and muted/secondary text.
        Consumed by the layout chrome (book.css / pageStyle), the search UI, the ToC
        resize-handle focus ring, and bare content links. These reuse the established
        panel / hairline / brand-blue palette and meet AA (4.5:1) for small text. */
    --verso-surface-color: #ffffff;
    --verso-border-color: #dbe2ea;
    --verso-link-color: #1c5fb8;
    --verso-muted-color: #4d5e6d;

    /** Message colors **/
    /*
    These colors are used to render Lean's feedback. They come in three severities and two
    variants. The raw color itself is used for the text of a message of the indicated severity,
    while the presence of such a message is indicated using the indicator color (e.g. via a
    wavy underline or a bar in the margin).
    */
    --verso-info-color: black;
    --verso-info-indicator-color: #4777ff;
    --verso-warning-color: black;
    --verso-warning-indicator-color: #e7a71d; /* 2.11 contrast ratio for white, 9.94 for black */
    --verso-error-color: #cc0000;
    --verso-error-indicator-color: #ff0000;

    /** Lean hover tooltip / goal-display surfaces **/
    /*
    Raised popover surfaces for Lean code hovers (tippy popovers + `.hover-info`)
    and the tactic goal display. Light defaults reproduce the historical
    hard-coded values (#e5e5e5 bg, black fg/border, white tactic bg); the dark
    scheme blocks below elevate them onto the #121c28 surface family. The rules
    in Highlighted.lean reference these with the same literals as `var()`
    fallbacks, so pages that don't load this file stay byte-identical in light.
    */
    --verso-hover-bg: #e5e5e5;
    --verso-hover-fg: black;
    --verso-hover-border: black;
    --verso-tactic-bg: #ffffff;

    /** Code Highlighting **/
    /*
    These variables control the rendering of Lean code emitted by Verso. Each category that can be
    highlighted supports the customization of color, weight, style, and family.
    */
    /*
    VSCode Light+ Lean palette (light defaults). The dark `data-bp-color-scheme`
    blocks below override these with the matching Dark+ values, and the explicit
    light block restores them so a forced-light choice beats OS dark. Stock
    Dark+/Light+ use no bold and no italic, so every weight/style here is normal.
    */
    /* Constants. Functions/values/theorems use the function color; Sort-valued constants (types)
       use the type color (VSCode Light+ entity.name.function / entity.name.type). The legacy
       `--verso-code-const-color` is retained for backwards compatibility. */
    --verso-code-const-color: #267f99;
    --verso-code-const-weight: normal;
    --verso-code-const-style: normal;
    --verso-code-const-font-family: var(--verso-code-font-family);
    --verso-code-function-color: #795e26;
    --verso-code-type-color: #267f99;

    /* Bracket-pair colorization (VSCode Light+ editorBracketHighlight defaults). Depths 0–2 are
       colored; depths 3–5 fall back to the code foreground (VSCode foreground4–6 are transparent).
       Unmatched brackets use the unexpected-bracket color. */
    --verso-code-bracket-depth-0: #0431FA;
    --verso-code-bracket-depth-1: #319331;
    --verso-code-bracket-depth-2: #7B3814;
    --verso-code-bracket-unexpected: rgba(255, 18, 18, 0.8);

    /* Keywords/atoms (e.g. `for` or `def` or `induction`) */
    --verso-code-keyword-color: #0000ff;
    --verso-code-keyword-weight: normal;
    --verso-code-keyword-style: normal;
    --verso-code-keyword-font-family: var(--verso-code-font-family);

    /* Local bindings (e.g. `x` in `let x := 5`) and wildcards */
    --verso-code-var-color: #001080;
    --verso-code-var-weight: normal;
    --verso-code-var-style: normal;
    --verso-code-var-font-family: var(--verso-code-font-family);

    /* Sorts (`Type`, `Prop`, `Sort`) */
    --verso-code-sort-color: #0000ff;
    /* String and character literals */
    --verso-code-string-color: #a31515;
    /* Numeric literals */
    --verso-code-number-color: #098658;
    /* Comments (line, block, doc, delimiters) */
    --verso-code-comment-color: #008000;
    /* Compiler options (e.g. `set_option`) */
    --verso-code-option-color: #0000ff;
}

/*
================================================================================
 Dark mode color scheme (orthogonal `data-bp-color-scheme` axis)
================================================================================
This is purely ADDITIVE. The bare `:root` above keeps the original light values,
so light mode is byte-for-byte identical to before by default.

Three layers, in increasing CSS specificity:
  1. `@media (prefers-color-scheme: dark) :root { … }`  (0,1,0) — OS "auto" dark.
  2. `:root[data-bp-color-scheme="dark"]  { … }`         (0,2,0) — manual dark.
  3. `:root[data-bp-color-scheme="light"] { … }`         (0,2,0) — manual light,
     which restores the light values so a forced-light choice wins over OS dark.

These overrides cover the core text/code/structure/message/selected tokens, the
Lean syntax-highlighting token colors, AND the layout vars used by book.css
(`pageStyle`) so the whole core chrome themes from one place. Keep the dark value
list in (1) and (2) in sync, and the light value list in (3) in sync with the
defaults above / in book.css's `:root`.
*/

/* Shared dark value list — applied for OS auto-dark. */
@media (prefers-color-scheme: dark) {
    :root {
        color-scheme: dark;

        /* Core text / code / structure */
        --verso-text-color: #dbe7f2;
        --verso-code-color: #d4d4d4;
        --verso-structure-color: #dbe7f2;
        --verso-background-color: #0e1722;

        /* Selected items (e.g. search results) */
        --verso-selected-color: #173049;

        /* UI surfaces, borders, links, and muted/secondary text */
        --verso-surface-color: #121c28;
        --verso-border-color: #22303f;
        --verso-link-color: #5aa0ff;
        --verso-muted-color: #c5cad6;

        /* Message colors */
        --verso-info-color: #dbe7f2;
        --verso-info-indicator-color: #64b5f6;
        --verso-warning-color: #dbe7f2;
        --verso-warning-indicator-color: #ffc107;
        --verso-error-color: #ff6b6b;
        --verso-error-indicator-color: #ff6b6b;

        /* Lean hover tooltip / goal-display surfaces (elevated onto the surface family) */
        --verso-hover-bg: #182432;
        --verso-hover-fg: #dbe7f2;
        --verso-hover-border: #33465a;
        --verso-tactic-bg: #182432;

        /* Lean syntax-highlighting token colors (VSCode Dark+) */
        --verso-code-const-color: #4ec9b0;
        --verso-code-function-color: #dcdcaa;
        --verso-code-type-color: #4ec9b0;
        --verso-code-bracket-depth-0: #FFD700;
        --verso-code-bracket-depth-1: #DA70D6;
        --verso-code-bracket-depth-2: #179FFF;
        --verso-code-bracket-unexpected: rgba(255, 18, 18, 0.8);
        --verso-code-keyword-color: #569cd6;
        --verso-code-keyword-weight: normal;
        --verso-code-var-color: #9cdcfe;
        --verso-code-var-style: normal;
        --verso-code-sort-color: #569cd6;
        --verso-code-string-color: #ce9178;
        --verso-code-number-color: #b5cea8;
        --verso-code-comment-color: #6a9955;
        --verso-code-option-color: #569cd6;

        /* Layout vars defined in book.css's :root */
        --verso-toc-background-color: #121c28;
        --verso-toc-border-color: #22303f;
        --verso-toc-resize-handle-color: #8a93b5;
        --verso-burger-toc-visible-shadow-color: #121c28;
        --verso-burger-toc-hidden-color: #dbe7f2;
        --verso-burger-toc-hidden-shadow-color: #121c28;

        /* Layout vars introduced for former hard-coded literals in book.css */
        --verso-header-bg: #121c28;
        --verso-header-shadow-color: rgba(0, 0, 0, 0.55);
        --verso-header-title-color: #dbe7f2;
        --verso-toc-backdrop-color: rgba(0, 0, 0, 0.6);
        --verso-toc-link-color: #c5cad6;
        --verso-toc-link-hover-color: #ffffff;
        --verso-toc-triangle-color: #dbe7f2;
        --verso-prev-next-color: #dbe7f2;
        --verso-info-border-color: #64b5f6;
    }
}

/* Same dark value list — applied for manual dark (overrides OS auto). */
:root[data-bp-color-scheme="dark"] {
    color-scheme: dark;

    --verso-text-color: #dbe7f2;
    --verso-code-color: #d4d4d4;
    --verso-structure-color: #dbe7f2;
    --verso-background-color: #0e1722;

    --verso-selected-color: #173049;

    --verso-surface-color: #121c28;
    --verso-border-color: #22303f;
    --verso-link-color: #5aa0ff;
    --verso-muted-color: #c5cad6;

    --verso-info-color: #dbe7f2;
    --verso-info-indicator-color: #64b5f6;
    --verso-warning-color: #dbe7f2;
    --verso-warning-indicator-color: #ffc107;
    --verso-error-color: #ff6b6b;
    --verso-error-indicator-color: #ff6b6b;

    /* Lean hover tooltip / goal-display surfaces (elevated onto the surface family) */
    --verso-hover-bg: #182432;
    --verso-hover-fg: #dbe7f2;
    --verso-hover-border: #33465a;
    --verso-tactic-bg: #182432;

    --verso-code-const-color: #4ec9b0;
    --verso-code-function-color: #dcdcaa;
    --verso-code-type-color: #4ec9b0;
    --verso-code-bracket-depth-0: #FFD700;
    --verso-code-bracket-depth-1: #DA70D6;
    --verso-code-bracket-depth-2: #179FFF;
    --verso-code-bracket-unexpected: rgba(255, 18, 18, 0.8);
    --verso-code-keyword-color: #569cd6;
    --verso-code-keyword-weight: normal;
    --verso-code-var-color: #9cdcfe;
    --verso-code-var-style: normal;
    --verso-code-sort-color: #569cd6;
    --verso-code-string-color: #ce9178;
    --verso-code-number-color: #b5cea8;
    --verso-code-comment-color: #6a9955;
    --verso-code-option-color: #569cd6;

    --verso-toc-background-color: #121c28;
    --verso-toc-border-color: #22303f;
    --verso-toc-resize-handle-color: #8a93b5;
    --verso-burger-toc-visible-shadow-color: #121c28;
    --verso-burger-toc-hidden-color: #dbe7f2;
    --verso-burger-toc-hidden-shadow-color: #121c28;

    --verso-header-bg: #121c28;
    --verso-header-shadow-color: rgba(0, 0, 0, 0.55);
    --verso-header-title-color: #dbe7f2;
    --verso-toc-backdrop-color: rgba(0, 0, 0, 0.6);
    --verso-toc-link-color: #c5cad6;
    --verso-toc-link-hover-color: #ffffff;
    --verso-toc-triangle-color: #dbe7f2;
    --verso-prev-next-color: #dbe7f2;
    --verso-info-border-color: #64b5f6;
}

/* Explicit light value list — restores defaults so manual light beats OS dark. */
:root[data-bp-color-scheme="light"] {
    color-scheme: light;

    --verso-text-color: #15212b;
    --verso-code-color: #15212b;
    --verso-structure-color: #15212b;
    --verso-background-color: #f4f6f8;

    --verso-selected-color: #e1ecf9;

    --verso-surface-color: #ffffff;
    --verso-border-color: #dbe2ea;
    --verso-link-color: #1c5fb8;
    --verso-muted-color: #4d5e6d;

    --verso-info-color: black;
    --verso-info-indicator-color: #4777ff;
    --verso-warning-color: black;
    --verso-warning-indicator-color: #e7a71d;
    --verso-error-color: #cc0000;
    --verso-error-indicator-color: #ff0000;

    /* Lean hover tooltip / goal-display surfaces (restore light defaults) */
    --verso-hover-bg: #e5e5e5;
    --verso-hover-fg: black;
    --verso-hover-border: black;
    --verso-tactic-bg: #ffffff;

    --verso-code-const-color: #267f99;
    --verso-code-function-color: #795e26;
    --verso-code-type-color: #267f99;
    --verso-code-bracket-depth-0: #0431FA;
    --verso-code-bracket-depth-1: #319331;
    --verso-code-bracket-depth-2: #7B3814;
    --verso-code-bracket-unexpected: rgba(255, 18, 18, 0.8);
    --verso-code-keyword-color: #0000ff;
    --verso-code-keyword-weight: normal;
    --verso-code-var-color: #001080;
    --verso-code-var-style: normal;
    --verso-code-sort-color: #0000ff;
    --verso-code-string-color: #a31515;
    --verso-code-number-color: #098658;
    --verso-code-comment-color: #008000;
    --verso-code-option-color: #0000ff;

    --verso-toc-background-color: #ffffff;
    --verso-toc-border-color: #dbe2ea;
    --verso-toc-resize-handle-color: #b4c0cc;
    --verso-burger-toc-visible-shadow-color: #ffffff;
    --verso-burger-toc-hidden-color: #15212b;
    --verso-burger-toc-hidden-shadow-color: #ffffff;

    --verso-header-bg: #ffffff;
    --verso-header-shadow-color: #dbe2ea;
    --verso-header-title-color: #15212b;
    --verso-toc-backdrop-color: #15212b66;
    --verso-toc-link-color: #4d5e6d;
    --verso-toc-link-hover-color: #15212b;
    --verso-toc-triangle-color: #15212b;
    --verso-prev-next-color: #15212b;
    --verso-info-border-color: #1c5fb8;
}