/* The syntax theme for Lean code shown on a surface that follows the site theme
   — the editor panes in the home page's audience sections. Verso's own
   highlighting leaves every token at `--color-text`, distinguishing keywords by
   weight alone, so a container that wants coloured code marks itself
   `.lean-themed` and the palettes below take over inside it.

   Two palettes, because the surface moves: VS Code's Light+ while the page is
   light, its Dark+ counterpart under `.dark-theme`. The Dark+ colours are the
   ones `.lean-dark` uses, so they live in `lean-dark.css`; this file holds the
   Light+ palette and the dark surface's own popup colour. Every light value
   clears 4.5:1 on white.

   The popups belong to the same theme but are appended to <body>, out of reach
   of that container, so `lean-popups.js` tags them with a matching tippy theme
   and they are styled here alongside the code they came from. `.dark-theme`
   sits on <html>, so the dark half still reaches them. */

/* ---------------------------------------------------------------------------
   Light
   --------------------------------------------------------------------------- */

.lean-themed .hl.lean .comment,
.lean-themed .hl.lean .doc-comment,
.tippy-box[data-theme~="lean-themed"] .hl.lean .comment,
.tippy-box[data-theme~="lean-themed"] .hl.lean .doc-comment {
    color: #2f7d4f !important;
}

.lean-themed .hl.lean .keyword,
.tippy-box[data-theme~="lean-themed"] .hl.lean .keyword {
    color: #8b21b8 !important;
}

/* `.sort` is `Prop` and `Type`, which read as the types they sit beside. */
.lean-themed .hl.lean .const,
.lean-themed .hl.lean .sort,
.tippy-box[data-theme~="lean-themed"] .hl.lean .const,
.tippy-box[data-theme~="lean-themed"] .hl.lean .sort {
    color: #267f99 !important;
}

.lean-themed .hl.lean .var,
.tippy-box[data-theme~="lean-themed"] .hl.lean .var {
    color: #001080 !important;
}

.lean-themed .hl.lean .literal,
.tippy-box[data-theme~="lean-themed"] .hl.lean .literal {
    color: #098658 !important;
}

.lean-themed .hl.lean .built-in,
.tippy-box[data-theme~="lean-themed"] .hl.lean .built-in {
    color: #795e26 !important;
}

/* Gated on a real pointer: on a touch screen `:hover` sticks to whatever was
   last tapped, which leaves one token highlighted until the next tap. */
@media (hover: hover) {
    .lean-themed .hl.lean .token.binding-hl,
    .lean-themed .hl.lean .literal:hover,
    .lean-themed .hl.lean .token.typed:hover,
    .lean-themed .hl.lean .tactic > label:hover {
        background-color: rgba(20, 40, 90, 0.08) !important;
    }
}

.lean-themed .hl.lean .tactic-state,
.lean-themed .hl.lean.popup .tactic-state {
    border-color: #dbe3ee;
    background: #f6f9fd !important;
    color: #24292f !important;
}

.tippy-box[data-theme~="lean-themed"] {
    border: 0;
    background-color: transparent;
}

.tippy-box[data-theme~="lean-themed"] .tippy-content {
    border: 1px solid #dbe3ee;
    border-radius: 8px;
    background: #fff;
    color: #24292f !important;
    box-shadow: 0 18px 40px rgba(30, 50, 120, 0.18);
}

.tippy-box[data-theme~="lean-themed"] .hl.lean .tactic-state,
.tippy-box[data-theme~="lean-themed"] .hl.lean.popup .tactic-state,
.tippy-box[data-theme~="lean-themed"] .hl.lean .hover-info code {
    background: #fff !important;
    color: #24292f !important;
}

/* Lean's own messages — the `#eval` results, the "All goals completed!" — are
   drawn on a card unless the popup carries the severity theme they expect,
   which the ones opened from a tactic block do not. */
.tippy-box[data-theme~="lean-themed"] .hl.lean .hover-info.messages > code {
    background: none !important;
}

.tippy-box[data-theme~="lean-themed"] .docstring,
.tippy-box[data-theme~="lean-themed"] .hl.lean .hover-info {
    color: #4b5563 !important;
}

.tippy-box[data-theme~="lean-themed"][data-placement^="top"] > .tippy-arrow::before {
    border-top-color: #fff !important;
}

.tippy-box[data-theme~="lean-themed"][data-placement^="bottom"] > .tippy-arrow::before {
    border-bottom-color: #fff !important;
}

.tippy-box[data-theme~="lean-themed"][data-placement^="left"] > .tippy-arrow::before {
    border-left-color: #fff !important;
}

.tippy-box[data-theme~="lean-themed"][data-placement^="right"] > .tippy-arrow::before {
    border-right-color: #fff !important;
}

/* ---------------------------------------------------------------------------
   Dark — the token colours are Dark+, shared with `.lean-dark` and kept in
   `lean-dark.css`; what is left here is this surface's own popup colour
   --------------------------------------------------------------------------- */

.dark-theme .lean-themed .hl.lean .tactic-state,
.dark-theme .lean-themed .hl.lean.popup .tactic-state {
    border-color: rgba(255, 255, 255, 0.14);
    background: #252526 !important;
    color: #dfe3ee !important;
}

.dark-theme .tippy-box[data-theme~="lean-themed"] .tippy-content {
    border-color: rgba(255, 255, 255, 0.12);
    background: #252526;
    color: #d4d4d4 !important;
    box-shadow: 0 18px 40px rgba(0, 0, 0, 0.55);
}

.dark-theme .tippy-box[data-theme~="lean-themed"] .hl.lean .tactic-state,
.dark-theme .tippy-box[data-theme~="lean-themed"] .hl.lean.popup .tactic-state,
.dark-theme .tippy-box[data-theme~="lean-themed"] .hl.lean .hover-info code {
    background: #252526 !important;
    color: #d4d4d4 !important;
}

.dark-theme .tippy-box[data-theme~="lean-themed"][data-placement^="top"] > .tippy-arrow::before {
    border-top-color: #252526 !important;
}

.dark-theme .tippy-box[data-theme~="lean-themed"][data-placement^="bottom"] > .tippy-arrow::before {
    border-bottom-color: #252526 !important;
}

.dark-theme .tippy-box[data-theme~="lean-themed"][data-placement^="left"] > .tippy-arrow::before {
    border-left-color: #252526 !important;
}

.dark-theme .tippy-box[data-theme~="lean-themed"][data-placement^="right"] > .tippy-arrow::before {
    border-right-color: #252526 !important;
}