/* Syntax highlighting for code blocks - Theme-aware */
/* Inherits colors from Pico.css for automatic dark mode support */

/* ============================================ */
/* Callout Blocks                              */
/* ============================================ */

.callout {
    padding: 1rem 1.5rem;
    margin: 1.5rem 0;
    border-left: 4px solid;
    border-radius: var(--pico-border-radius, 0.25rem);
    background-color: var(--pico-card-background-color);
}

.callout > :first-child {
    margin-top: 0;
}

.callout > :last-child {
    margin-bottom: 0;
}

.callout-note {
    border-left-color: var(--pico-primary);
    background-color: color-mix(in srgb, var(--pico-primary) 10%, var(--pico-background-color));
}

.callout-info {
    border-left-color: #3b82f6;
    background-color: color-mix(in srgb, #3b82f6 10%, var(--pico-background-color));
}

.callout-tip {
    border-left-color: #10b981;
    background-color: color-mix(in srgb, #10b981 10%, var(--pico-background-color));
}

.callout-warning {
    border-left-color: #f59e0b;
    background-color: color-mix(in srgb, #f59e0b 10%, var(--pico-background-color));
}

.callout-danger {
    border-left-color: #ef4444;
    background-color: color-mix(in srgb, #ef4444 10%, var(--pico-background-color));
}

/* Margin callouts - appear to the right of content */
.callout-margin {
    position: absolute;
    right: -400px;
    width: 350px;
    margin: 0.5rem 0;
    padding: 0.75rem 1rem;
    font-size: 0.875rem;
    line-height: 1.5;
}

/* Add extra space between consecutive margin notes */
.callout-margin + * + .callout-margin {
    margin-top: 3rem;
}

/* On smaller screens, display inline with visual distinction */
@media (max-width: 1200px) {
    .callout-margin {
        position: static;
        right: auto;
        width: auto;
        margin: 1.5rem 0 1.5rem 2rem;
        padding: 1rem 1.5rem;
        font-size: 0.95rem;
        border-left: 3px solid var(--pico-primary);
        font-style: italic;
    }
}

.dafny-code {
    padding: 8px 8px;
    margin: 2.0rem auto;
    background-color: var(--pico-code-background-color);
    border: 1px solid var(--pico-muted-border-color);
    overflow-x: auto;
    white-space: pre;
    font-family: var(--pico-font-family-monospace, monospace);
    line-height: 1.4;
    color: var(--pico-color);
}

.dafny-code pre {
    padding: 0;
    margin: 0;
    border: none;
    background: transparent;
    overflow-x: auto;
    white-space: pre;
}

/* Line structure */
.dafny-code .line { display: block; }
.dafny-code .cl { display: contents; }

/* Keywords - use primary color */
.dafny-code .k,
.dafny-code .kc,
.dafny-code .kd,
.dafny-code .kp,
.dafny-code .kr,
.dafny-code .kt {
    color: var(--pico-primary);
    font-weight: 600;
}

/* Special keywords - use contrast color */
.dafny-code .kn {
    color: var(--pico-contrast);
    font-weight: 600;
}

/* Strings and literals - use secondary color with fallback */
.dafny-code .s,
.dafny-code .s1,
.dafny-code .s2,
.dafny-code .sa,
.dafny-code .sb,
.dafny-code .sc,
.dafny-code .dl,
.dafny-code .sd,
.dafny-code .se,
.dafny-code .sh,
.dafny-code .si,
.dafny-code .sx,
.dafny-code .sr,
.dafny-code .ss,
.dafny-code .l,
.dafny-code .ld {
    color: var(--pico-secondary, var(--pico-primary-hover));
}

/* Numbers - slightly emphasized */
.dafny-code .m,
.dafny-code .mb,
.dafny-code .mf,
.dafny-code .mh,
.dafny-code .mi,
.dafny-code .il,
.dafny-code .mo {
    color: var(--pico-secondary, var(--pico-primary-hover));
    font-weight: 600;
}

/* Comments - muted color */
.dafny-code .c,
.dafny-code .c1,
.dafny-code .ch,
.dafny-code .cm,
.dafny-code .cs,
.dafny-code .cp,
.dafny-code .cpf {
    color: var(--pico-muted-color);
    font-style: italic;
}

/* Names, identifiers, functions - inherit main text color */
.dafny-code .n,
.dafny-code .na,
.dafny-code .nb,
.dafny-code .bp,
.dafny-code .nc,
.dafny-code .no,
.dafny-code .nd,
.dafny-code .ni,
.dafny-code .ne,
.dafny-code .nf,
.dafny-code .fm,
.dafny-code .nl,
.dafny-code .nn,
.dafny-code .nx,
.dafny-code .py,
.dafny-code .nt,
.dafny-code .nv,
.dafny-code .vc,
.dafny-code .vg,
.dafny-code .vi,
.dafny-code .vm {
    color: var(--pico-color);
}

/* Operators and punctuation - inherit main text color */
.dafny-code .o,
.dafny-code .ow,
.dafny-code .p {
    color: var(--pico-color);
}

/* Generic/special - use contrast */
.dafny-code .g,
.dafny-code .gd,
.dafny-code .ge,
.dafny-code .gr,
.dafny-code .gh,
.dafny-code .gi,
.dafny-code .go,
.dafny-code .gp,
.dafny-code .gs,
.dafny-code .gu,
.dafny-code .gt,
.dafny-code .gl {
    color: var(--pico-contrast);
}

/* ============================================ */
/* MathJax Equation Overflow Handling         */
/* ============================================ */

/* Make display equations scrollable when they overflow */
mjx-container[display="true"] {
    overflow-x: auto;
    overflow-y: hidden;
    max-width: 100%;
    display: block !important;
    margin: 1.5rem 0;
    padding: 0.5rem;
    background-color: var(--pico-card-background-color, transparent);
    border-radius: var(--pico-border-radius, 0.25rem);
}

/* Add a subtle shadow to indicate scrollability */
mjx-container[display="true"]::-webkit-scrollbar {
    height: 8px;
}

mjx-container[display="true"]::-webkit-scrollbar-track {
    background: var(--pico-form-element-background-color);
    border-radius: 4px;
}

mjx-container[display="true"]::-webkit-scrollbar-thumb {
    background: var(--pico-muted-border-color);
    border-radius: 4px;
}

mjx-container[display="true"]::-webkit-scrollbar-thumb:hover {
    background: var(--pico-primary);
}

/* Ensure inline math doesn't cause issues */
mjx-container[display="false"] {
    display: inline-block;
}

/* ============================================ */
/* Lean Proof State Blocks                     */
/* ============================================ */

.lean-proof-block {
    margin: 1rem 0;
}

.lean-proof-block > pre.proof-code {
    margin-bottom: 0;
    border-bottom: none;
    border-bottom-left-radius: 0;
    border-bottom-right-radius: 0;
}

/* Proof state card */
.lean-proof-block .proof-state {
    border-left: 3px solid var(--syntax-builtin, #005cc5);
    border-right: 1px solid var(--pico-muted-border-color);
    border-bottom: 1px solid var(--pico-muted-border-color);
    border-bottom-left-radius: var(--pico-border-radius, 0.25rem);
    border-bottom-right-radius: var(--pico-border-radius, 0.25rem);
    background-color: color-mix(in srgb, var(--syntax-builtin, #005cc5) 5%, var(--pico-code-background-color));
    font-family: "JetBrains Mono", var(--pico-font-family-monospace, monospace);
    /* Match Pico's <pre> font-size so inner code compounding is identical */
    font-size: 0.875em;
    line-height: 1.55;
}

.lean-proof-block .proof-state code {
    font-size: 0.88em;
    font-family: inherit;
    line-height: inherit;
    background: none;
    padding: 0;
}

/* Header with goal count badge */
.lean-proof-block .proof-state-header {
    padding: 0.35rem 0.75rem;
    border-top: 1px dashed var(--pico-muted-border-color);
}

.lean-proof-block .proof-goal-badge {
    display: inline-block;
    padding: 0.1rem 0.5rem;
    font-size: 0.75em;
    font-family: var(--pico-font-family, sans-serif);
    font-variant: small-caps;
    letter-spacing: 0.05em;
    color: var(--syntax-builtin, #005cc5);
    background-color: color-mix(in srgb, var(--syntax-builtin, #005cc5) 10%, var(--pico-code-background-color));
    border: 1px solid color-mix(in srgb, var(--syntax-builtin, #005cc5) 20%, var(--pico-muted-border-color));
    border-radius: 1rem;
}

/* Hypothesis rows */
.lean-proof-block .proof-hypotheses {
    padding: 0.25rem 0.75rem;
}

.lean-proof-block .proof-hyp:nth-child(even) {
    background-color: color-mix(in srgb, var(--syntax-builtin, #005cc5) 3%, transparent);
    margin: 0 -0.75rem;
    padding-left: 0.75rem;
    padding-right: 0.75rem;
}

.lean-proof-block .proof-hyp code {
    white-space: pre-wrap;
}

/* Goal block grouping (case header + hyps + goal) */
.lean-proof-block .proof-goal-block + .proof-goal-block {
    border-top: 1px dashed color-mix(in srgb, var(--syntax-builtin, #005cc5) 20%, var(--pico-muted-border-color));
}

/* Case header */
.lean-proof-block .proof-case-header {
    padding: 0.3rem 0.75rem 0.15rem;
    font-size: 0.8em;
    font-weight: 600;
    color: var(--syntax-builtin, #005cc5);
}

.lean-proof-block .proof-case-header code {
    font-weight: inherit;
    color: inherit;
}

/* Goal section */
.lean-proof-block .proof-goal {
    padding: 0.4rem 0.75rem;
    border-top: 1px solid color-mix(in srgb, var(--syntax-builtin, #005cc5) 25%, transparent);
    background-color: color-mix(in srgb, var(--syntax-builtin, #005cc5) 10%, var(--pico-code-background-color));
    border-bottom-left-radius: var(--pico-border-radius, 0.25rem);
    border-bottom-right-radius: var(--pico-border-radius, 0.25rem);
}

.lean-proof-block .proof-goal-line code {
  white-space: pre;
  padding: 0;
}

/* Make the turnstile symbol more prominent */
.lean-proof-block .proof-goal .token.operator:first-child {
    font-size: 1.15em;
    font-weight: 700;
    color: var(--syntax-builtin, #005cc5);
}

/* In the structured proof pane, hide the +/-/space diff prefix character;
   the line background already signals what changed. */
.lean-proof-block .proof-hyp .token.prefix,
.lean-proof-block .proof-goal .token.prefix,
.lean-proof-block .proof-case-header .token.prefix {
    display: none;
}


/* ============================================ */
/* Prism.js Syntax Highlighting - Theme-aware  */
/* ============================================ */

/* Code blocks generated by Prism */
pre[class*="language-"] {
    background-color: var(--pico-code-background-color);
    border: 1px solid var(--pico-muted-border-color);
    border-radius: var(--pico-border-radius, 0.25rem);
    padding: 0rem;
    margin: 1rem 0;
    overflow-x: auto;
    color: var(--pico-color);
}

code {
    padding: 0.1em
}

code[class*="language-"] {
    color: var(--pico-color);
    font-family: "JetBrains Mono", var(--pico-font-family-monospace, monospace);
    font-size: 0.88em;
    line-height: 1.55;
}

/* Inline code (not in pre blocks) */
:not(pre) > code[class*="language-"] {
    background-color: var(--pico-code-background-color);
    padding: 0.1em 0.3em;
    border-radius: 0.25rem;
}

/* Token colors - Modern syntax highlighting theme */
/* Light mode colors */
:root:not([data-theme="dark"]) {
    --syntax-comment: #6a737d;
    --syntax-keyword: #d73a49;
    --syntax-string: #22863a;
    --syntax-number: #005cc5;
    --syntax-function: #6f42c1;
    --syntax-class: #6f42c1;
    --syntax-operator: #d73a49;
    --syntax-punctuation: #24292e;
    --syntax-builtin: #005cc5;
    --syntax-variable: #e36209;
}

/* Dark mode colors */
@media (prefers-color-scheme: dark) {
    :root:not([data-theme="light"]) {
        --syntax-comment: #8b949e;
        --syntax-keyword: #ff7b72;
        --syntax-string: #a5d6ff;
        --syntax-number: #79c0ff;
        --syntax-function: #d2a8ff;
        --syntax-class: #ffa657;
        --syntax-operator: #ff7b72;
        --syntax-punctuation: #c9d1d9;
        --syntax-builtin: #79c0ff;
        --syntax-variable: #ffa657;
    }
}

.token.comment,
.token.prolog,
.token.doctype,
.token.cdata {
    color: var(--syntax-comment);
    font-style: italic;
}

.token.punctuation {
    color: var(--syntax-punctuation);
    opacity: 0.7;
}

.token.property,
.token.tag,
.token.boolean,
.token.constant,
.token.symbol,
.token.deleted {
    color: var(--syntax-keyword);
}

.token.number {
    color: var(--syntax-number);
    font-weight: 600;
}

.token.selector,
.token.attr-name,
.token.string,
.token.char,
.token.inserted {
    color: var(--syntax-string);
}

.token.builtin {
    color: var(--syntax-builtin);
    font-weight: 600;
}

.token.operator,
.token.entity,
.token.url,
.language-css .token.string,
.style .token.string {
    color: var(--syntax-operator);
}

.token.atrule,
.token.attr-value,
.token.keyword {
    color: var(--syntax-keyword);
    font-weight: 600;
}

.token.function {
    color: var(--syntax-function);
}

.token.class-name {
    color: var(--syntax-class);
}

.token.regex,
.token.important,
.token.variable {
    color: var(--syntax-variable);
}

.token.important,
.token.bold {
    font-weight: bold;
}

.token.italic {
    font-style: italic;
}

/* Diff line highlighting — ```diff and ```diff-<lang> code fences. */
.token.deleted:not(.prefix) {
    background-color: color-mix(in srgb, #ef4444 15%, transparent);
}

.token.inserted:not(.prefix) {
    background-color: color-mix(in srgb, #10b981 15%, transparent);
}

.token.prefix.deleted {
    color: #ef4444;
    font-weight: 600;
}

.token.prefix.inserted {
    color: #10b981;
    font-weight: 600;
}