:root {
    --verso-structure-font-family: "Helvetica Neue","Segoe UI",Arial,sans-serif;
    --verso-text-font-family: Source Serif, Georgia,Times,"Times New Roman",serif;
    --verso-code-font-family: Source Code Pro, monospace;
}

p {
    font-feature-settings: "calt" off;
}

section > p, section > ul, section > ol {
    margin-top: 1rem;
    margin-bottom: 1rem;
}

div.paragraph > p:not(:first-child),
div.paragraph > ul:not(:first-child),
div.paragraph > ol:not(:first-child),
div.paragraph > dl:not(:first-child) {
  margin-top: 0.5rem;
}

div.paragraph > p:not(:last-child),
div.paragraph > ul:not(:last-child),
div.paragraph > ol:not(:last-child),
div.paragraph > dl:not(:last-child) {
  margin-bottom: 0.5rem;
}

/*
Don't impose margins on lists or list items from their contents.
*/
li > :first-child {
  margin-top: 0;
}
li > :last-child {
  margin-bottom: 0;
}

li:not(:first-child) {
  margin-top: 0.5rem;
}
li:not(:last-child) {
  margin-bottom: 0.5rem;
}

/* Lean-Code in dezenten grauen Kästen, wie auf verso.lean-lang.org */
.hl.lean.block {
    display: block;
    margin-top: 1em;
    margin-bottom: 1em;
    padding: 0.75em 1em;
    background-color: #f6f7f8;
    border: 1px solid #e1e4e8;
    border-radius: 0.4em;
    overflow-x: auto;
}

/* Lean-Bezeichner im Fließtext (`code`-Spannen) ebenfalls dezent
   hinterlegen — die andere Schriftart allein hebt sie zu wenig ab.
   Ausgenommen: Mathe-Formeln (KaTeX), Highlighter-Blöcke, Meldungen. */
code:not(.math):not([class~="hl"]):not(.verso-message):not(.docstring) {
    background-color: #f6f7f8;
    border: 1px solid #e1e4e8;
    border-radius: 0.25em;
    padding: 0.05em 0.3em;
}

/* Innerhalb von Codeblöcken, Tooltips und Meldungen kein zweiter Kasten */
.hl.lean code,
.verso-message code,
pre code {
    background-color: transparent;
    border: none;
    padding: 0;
}

/* Skript-Zitate (Sätze, Definitionen, Beweise) in umrandeten Kästen */
blockquote {
    margin: 1.25em 0;
    padding: 0.75em 1em;
    border: 1px solid var(--lean-accent-light-blue);
    border-left: 0.25em solid var(--lean-blue);
    border-radius: 0.25em;
    background-color: #f5f9fb;
}

blockquote > :first-child {
    margin-top: 0;
}

blockquote > :last-child {
    margin-bottom: 0;
}

/* Syntax-Farben für Lean-Code, angelehnt an das Light+-Thema von
   VS Code (Standardansicht des Lean-Plugins).  Versos Highlighter
   klassifiziert jedes Token semantisch; hier bekommt jede Klasse
   ihre Farbe. */
.hl.lean .keyword.token {
    font-weight: 600;
    color: #0000c0;          /* theorem, by, fun, … */
}

.hl.lean .const.token {
    color: #795e26;          /* Konstanten: Lemmanamen, ℤ, Ideal, … */
}

.hl.lean .var.token {
    color: #001080;          /* gebundene Variablen */
}

.hl.lean .sort.token {
    color: #267f99;          /* Type, Prop */
}

.hl.lean .literal.token {
    color: #098658;          /* Zahl- und String-Literale */
}

.hl.lean .comment.token {
    color: #007000;          /* Kommentare — die Skript-Sätze */
    font-style: italic;
}

.hl.lean .wildcard.token {
    color: #708090;          /* Unterstriche/Platzhalter */
}

figure {
    padding: 0;
    margin: 1em 0;
}

figure img {
    width: 100%;
    max-height: 75vh; /* No scrolling! */
}


figcaption {
    font-family: var(--verso-structure-font-family);
    text-align: center;
}

.error pre, .information pre, .warning pre,
.error code, .information code, .warning code {
    overflow-x: auto;
    margin: 0px;
}

.information pre, .error pre, .warning pre,
.information code, .error code, .warning code {
  margin: 0.5em .85em;
  border-left: 0.2em solid red;
  padding: 0 0.45em;
}

/* Different color for warning */
.warning pre, .warning code {
    border-color: #efd871;
}

/* Different color for information */
.information pre, .information code {
    border-color: #0000c0;
}

/* TODO: fix upstream */
.hl.lean code {
    font-family: var(--verso-code-font-family) !important;
}