/* The syntax theme for Lean code shown on a dark surface: VS Code's Dark+.
   Verso's own highlighting is written for light pages, where every token
   defaults to black, so a container that shows its code dark takes the palette
   below.

   Two containers use it. `.lean-dark` is dark in both site themes: it is put on
   the `.post-content` of guides and articles, whose code panes are styled at
   the end of this file. `.lean-themed`, the home page's editor panes, follows
   the site theme and takes this palette under `.dark-theme`; its light palette
   and its own popup surface are in `lean-themed.css`.

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

.lean-dark .hl.lean span,
.lean-dark .inter-text,
.dark-theme .lean-themed .hl.lean span,
.dark-theme .lean-themed .inter-text,
.tippy-box[data-theme~="lean-dark"] .hl.lean span,
.tippy-box[data-theme~="lean-dark"] .inter-text,
.dark-theme .tippy-box[data-theme~="lean-themed"] .hl.lean span,
.dark-theme .tippy-box[data-theme~="lean-themed"] .inter-text {
    color: #d4d4d4 !important;
}

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

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

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

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

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

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

/* Verso styles its hover highlights and proof-state boxes for light pages.
   The highlights are 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-dark .hl.lean .token.binding-hl,
    .lean-dark .hl.lean .literal:hover,
    .lean-dark .hl.lean .token.typed:hover,
    .lean-dark .hl.lean .tactic > label:hover,
    .dark-theme .lean-themed .hl.lean .token.binding-hl,
    .dark-theme .lean-themed .hl.lean .literal:hover,
    .dark-theme .lean-themed .hl.lean .token.typed:hover,
    .dark-theme .lean-themed .hl.lean .tactic > label:hover {
        background-color: rgba(255, 255, 255, 0.13) !important;
    }
}

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

/* ---------------------------------------------------------------------------
   The `.lean-dark` surface: proof states and popups
   --------------------------------------------------------------------------- */

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

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

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

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

/* Lean's own messages — the `#eval` results, the "All goals completed!" — are
   drawn on a light 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-dark"] .hl.lean .hover-info.messages > code {
    background: none !important;
}

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

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

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

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

/* ---------------------------------------------------------------------------
   Code panes in guides and articles
   --------------------------------------------------------------------------- */

/* Code is shown the way an editor shows it — a dark pane with real syntax
   colours — rather than as the article's light code card. Every other block
   (a project tree, a terminal transcript, an `#eval` result) is a plain
   `<pre>`, which takes the same pane so that it does not read as a different
   kind of thing beside the Lean; only its text colour has to be stated, since
   nothing inside it is highlighted for the palette to recolour. */
.post-content.lean-dark code.hl.lean.block,
.post-content.lean-dark pre {
    padding: var(--space-6);
    border: 1px solid;
    border-radius: var(--radius-md);
    font-size: 0.95rem;
}

/* The colours are restated under `.dark-theme`, where the article's dark cards
   are more specific. Only the colour of the border: the article joins
   consecutive blocks by removing the edge between them. */
.post-content.lean-dark code.hl.lean.block,
.post-content.lean-dark pre,
:root.dark-theme .post-content.lean-dark code.hl.lean.block,
:root.dark-theme .post-content.lean-dark pre {
    border-color: #232838;
    background: #0b0e16;
    color: #d4d4d4;
}

/* An `#eval` result or a message below a snippet keeps the coloured edge Verso
   marks its severity with. After the panes, which these tie with under
   `.dark-theme`. */
.post-content.lean-dark pre.lean-output.information {
    border-left: 0.2em solid var(--verso-output-info-color, var(--verso-info-indicator-color, #4777ff));
}

.post-content.lean-dark pre.lean-output.warning {
    border-left: 0.2em solid var(--verso-output-warning-color, var(--verso-warning-indicator-color, #e7a71d));
}

.post-content.lean-dark pre.lean-output.error {
    border-left: 0.2em solid var(--verso-output-error-color, var(--verso-error-indicator-color, #ff0000));
}

/* Inline Lean is a chip of the same pane, so a name in a sentence matches the
   colour it has in the snippet below. */
.post-content.lean-dark p code.hl.lean:not(.math),
:root.dark-theme .post-content.lean-dark p code.hl.lean:not(.math) {
    border-color: #232838;
    background: #0b0e16;
}

/* The copy and Playground buttons hung off a code block are painted from the
   page's surface tokens, which are the light page's — but they sit on the
   pane. Opaque, not a wash of white over it: a button floats above the code it
   overlaps, and a translucent one is read through. */
.post-content.lean-dark .copy-button,
.post-content.lean-dark .code-block-actions .playground-button {
    border-color: #2c3346;
    background: #141a29;
    color: #e8eaf0;
}

.post-content.lean-dark .copy-button:hover,
.post-content.lean-dark .code-block-actions .playground-button:hover {
    border-color: var(--color-primary-light);
    background: #1d2438;
    color: var(--color-primary-light);
}

@media (max-width: 768px) {
    .post-content.lean-dark code.hl.lean.block,
    .post-content.lean-dark pre {
        padding: var(--space-4);
    }
}