/*
 * LPdoc stylesheet for the HTML backend (+playground components)
 *
 * (c) 2018-2024 The Ciao Development Team
 */

/* --------------------------------------------------------------------------- */
/* Color theme */

html {
    --bg: #FFFFFF;
    --fg: #000000;
    --sidebar-link: #4263ab;
    --link-fg: #4263ab;
    --code-fg: #666;
    --code-bg: #f7f7f7;
    --codeblock-bg: #fff8dd;
    --codeblock-border: #fbe89d;
    --var-fg: #e06000;
    --border: #EEE;
    --rule: #999;
    --fgdim: #888;
    --header: #2e4985;
    --defname-bg: #eee;
    --note-accent: #b6cbdc;
    --note-bg: #f5f8f9;
    --note-border: #ebf3f9;
    --alert-accent: #ff8282;
    --alert-bg: #fffafa;
    --alert-border: #f9ebed;
    --cartouche-border: #c8e2f0;
    --cartouche-bg: #eff6fc;
    --cartouche-fg: #1d609a;
    --dropdown-bg: whitesmoke;
    --dropdown-sep: #C4C4C4;
    --scrollbar-thumb: #b0b0b0;
    --button-bg: rgb(239, 239, 239);
    --button-color: #111111;
    --button-border: lightgray;
    --button-border-hover: #B0B0B0;
}

html[data-theme='dark'] {
    color-scheme: dark;
    --bg: #23272D;
    --fg: #AFBAC6;
    --sidebar-link: #73869c;
    --link-fg: #5c9cec;
    --code-fg: #AFBAC6;
    --code-bg: #2E333A;
    --codeblock-bg: #2E333A;
    --codeblock-border: #2E333A;
    --var-fg: #fdce56;
    --border: #383838;
    --rule: #646b74;
    --fgdim: #747b84;
    --header: #E0E0E0;
    --defname-bg: #1e2125;
    --note-accent: #0085fa;
    --note-bg: #172531;
    --note-border: #01396a;
    --alert-accent: #ff6060;
    --alert-bg: #33272D;
    --alert-border: #53272D;
    --cartouche-border: #2e333b; /* #23334d */
    --cartouche-bg: #1e2125; /* #1b2432 */
    --cartouche-fg: #a8dbff; /* #9bdcf3 */
    --dropdown-bg: #000000;
    --dropdown-sep: #474D55;
    --scrollbar-thumb: #39414c;
    --button-bg: #000000;
    --button-color: white;
    --button-border: #000000;
    --button-border-hover: #3b4756;
}

::-webkit-scrollbar {
    background: var(--bg);
}
::-webkit-scrollbar-thumb {
    background: var(--scrollbar-thumb);
}
::-webkit-scrollbar-corner {
    background: var(--bg);
}
html {
    scrollbar-color: var(--scrollbar-thumb) var(--bg);
}

body, html {
    margin:0;
    padding:0;
    font-family: -apple-system,Helvetica,Arial,sans-serif;
    font-size: 16px;
    line-height: 1.3em;
    color: var(--fg);
    background-color: var(--bg);
}

/* --------------------------------------------------------------------------- */
/* Language and documentation elements */

.lpdoc-defname {
    font-size: 105%;
    font-weight:bold;
    background-color: var(--defname-bg);
    padding: 3px 8px 3px 8px;
    border-radius: 3px;
}

.lpdoc-deftext {
    padding-top: 0.5em;
    padding-bottom: 0.5em;
    padding-left: 16px;
}

.lpdoc-on-right {
    float: right;
}

.lpdoc-iso {
    color: #ffffff;
    background-color: #48d;
    /* text-shadow: 0px 1px 2px #000000; */
    font-size: 80%;
    padding-left: 4px; padding-right: 4px;
    border-radius: 4px;
}

.lpdoc-emacskey {
    border-radius: 3px;
/*    border-bottom: 1px solid #666;*/
/*    border-left: 1px solid #666;*/
/*    border-right: 1px solid #666;*/
/*    border-top: 1px solid #888;*/
    background-color: #444;
    font-size: 14px;
    font-family: -apple-system,Helvetica,Arial,sans-serif;
    font-weight: normal;
    color: #ffffff;
    text-shadow: 0px 0px 2px #000000;
    padding-top: 1px;
    padding-bottom: 1px;
    padding-left: 4px;
    padding-right: 4px;
}

.lpdoc-itemize-none {
    list-style-type: none;
}

.lpdoc-itemize-plain {
    list-style-type: none;
    padding-left: 0px;
}

.lpdoc-itemize-minus {
    list-style-type: circle;
}

/* Font sizes (@small{...}, @begin{Large}, ...). As in LaTeX, each is
   a factor of the normal text size, not of the size around it, so
   sizes do not compound. Code blocks, whose size is fixed in pixels,
   are scaled by the same factor. */
.lpdoc-fontsize-tiny         { --lpdoc-fontsize: 0.5; }
.lpdoc-fontsize-scriptsize   { --lpdoc-fontsize: 0.7; }
.lpdoc-fontsize-footnotesize { --lpdoc-fontsize: 0.8; }
.lpdoc-fontsize-small        { --lpdoc-fontsize: 0.9; }
.lpdoc-fontsize-normalsize   { --lpdoc-fontsize: 1; }
.lpdoc-fontsize-large        { --lpdoc-fontsize: 1.2; }
.lpdoc-fontsize-Large        { --lpdoc-fontsize: 1.44; }
.lpdoc-fontsize-LARGE        { --lpdoc-fontsize: 1.728; }
.lpdoc-fontsize-huge         { --lpdoc-fontsize: 2.074; }
.lpdoc-fontsize-Huge         { --lpdoc-fontsize: 2.488; }

.lpdoc-fontsize {
    font-size: calc(var(--lpdoc-fontsize) * 1rem);
    line-height: 1.3em; /* body's 1.3em is inherited as a fixed length */
}
/* Inline code is smaller than the text (see below), in every size */
tt .lpdoc-fontsize, code .lpdoc-fontsize, .lpdoc-var .lpdoc-fontsize {
    font-size: calc(var(--lpdoc-fontsize) * 0.85rem);
}
/* The editor of runnable code sets its own font size, so it is zoomed */
.lpdoc-fontsize .lpdoc-runnable-container {
    zoom: var(--lpdoc-fontsize);
}

pre.lpdoc-codeblock {
    font-family: SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;
    font-size: calc(14px * var(--lpdoc-fontsize, 1));
    line-height: normal;
    padding: 8px;
    background-color: var(--codeblock-bg);
    border: 1px solid var(--codeblock-border);
    border-radius: 3px;
    overflow-x: auto;
}

pre.lpdoc-codeblock .lpdoc-var,
pre.lpdoc-codeblock tt,
pre.lpdoc-codeblock code {
    background: none;
}

pre.lpdoc-codeblock tt,
pre.lpdoc-codeblock code {
    color: var(--fg);
}

.lpdoc-var, pre, tt, code {
    font-family: SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;
    font-size: 85%;
}

.lpdoc-var {
    color: var(--var-fg);
}
tt, code {
    color: var(--code-fg);
}
.lpdoc-var, tt, code {
    padding: 0.2em 0.3em;
    border-radius: 3px;
    background-color: var(--code-bg);
}

/* Assertion status tags (on the right) */
span.lpdoc-true-header,
span.lpdoc-false-header,
span.lpdoc-check-header,
span.lpdoc-checked-header,
span.lpdoc-trust-header {
    color: var(--bg);
    padding: 3px 8px 3px 8px;
    margin-left: 4px;
    border-radius: 3px;
    float: right;
}

/* Name tag for true assertions (in green) */
span.lpdoc-true-header { background-color: #78ac2b; }
/* Name tag for false assertions (in red) */
span.lpdoc-false-header { background-color: #ff6262; }
/* Name tag for check assertions (including Usage) (in blue) */
span.lpdoc-check-header { background-color: #3f8cdc; }
/* Name tag for checked assertions (in lightest green) */
span.lpdoc-checked-header { background-color: #6eb88c; }
/* Name tag for trust assertions (in orange) */
span.lpdoc-trust-header { background-color: #ffa162; }

/* E.g., "Usage 1" */
span.lpdoc-usage-header {
    font-weight: bold;
    padding-right: 8px;
}

/* E.g., foo(+,-,+) */
span.lpdoc-usage-decl {
    /* background-color: #eee; */
    background-color: var(--cartouche-bg); /* like mod usage */
    color: var(--cartouche-fg);
    padding: 3px 8px 3px 8px;
    /* border-radius: 0px 3px 3px 0px; */
    border-radius: 3px;
    line-height: 1.6em; /* TODO: better way? (avoid some overlap in narrow windows) */
}
span.lpdoc-usage-decl .lpdoc-var,
span.lpdoc-usage-decl tt,
span.lpdoc-usage-decl code {
    background: none;
    color: var(--cartouche-fg);
}

/* Tag for predicates (PREDICATE, REGTYPE, etc.) */
span.lpdoc-predtag {
    font-size: 14px;
    font-weight: bold;
    color: var(--fgdim);
    /* background-color: #eee; */
    /* padding: 3px 8px 3px 8px; */
    /* border-radius: 3px; */
    padding-right: 8px;
    /* float: right; */ /* on the right (unused) */
}

/* Images: keep one that is wider than the text column from making the
   whole page scroll sideways. lpdoc does not wrap images inside
   anything (would be heavier), so without this the overflow
   propagates out to the document body.  The forms that leave a
   dimension empty emit no height attribute at all, so they keep their
   aspect ratio under this rule; only when both dimensions are given
   the image is distorted when clamped; this is a price to pay when
   asking for an exact size in a window too narrow for it. */
.lpdoc-main img {
    max-width: 100%;
}

/* MathJax: its HTML-CSS output ends every expression with a zero-width
   "strut" span carrying border-left-style:solid in the text colour.
   The width computes to 0, so it should never paint, but under
   sub-pixel rounding (slide mode scales the page with CSS zoom) it can
   show up as a hairline to the right of each formula. Removing the
   border style leaves the strut's metrics, and the expression, intact.
   !important is required: the strut carries the border in an inline
   style attribute, which otherwise wins over this rule. */
.MathJax span[style*="border-left"] {
    border-left-style: none !important;
}

/* --------------------------------------------------------------------------- */
/* Special blocks */

/* Quotations (@begin{quotation}, or "> " in markdown). Deliberately
   quieter than a cartouche: a rule on the left rather than a frame, so
   that a quoted passage does not read as an aside or a warning. Its
   text is as readable as the rest (it is content, e.g., a problem
   statement): the rule and the indentation are what set it off. */
.lpdoc-quote {
    margin: 0.8em 0 0.8em 0;
    padding: 0.2em 0 0.2em 1em;
    border-left: 3px solid var(--fgdim);
    color: var(--fg);
}

.lpdoc-cartouche {
    border: 1px solid var(--cartouche-border);
    border-radius: 3px;
    padding: 8px;
    background-color: var(--cartouche-bg);
}
.lpdoc-cartouche .lpdoc-var,
.lpdoc-cartouche tt,
.lpdoc-cartouche code {
    background: none;
    color: var(--cartouche-fg);
}

/* ul immediate child of cartouche */
.lpdoc-cartouche > ul {
    margin: 8px;
    padding: 0px;
    list-style-type: none;
}

.lpdoc-note {
    border: 1px solid var(--note-border);
    border-left: 5px solid var(--note-accent);
    padding: 8px;
    border-radius: 3px;
    color: var(--fg);
    background-color: var(--note-bg);
}
.lpdoc-alert {
    border: 1px solid var(--alert-border);
    border-left: 5px solid var(--alert-accent);
    padding: 8px;
    border-radius: 3px;
    color: var(--fg);
    background-color: var(--alert-bg);
}

/* An item with a label of its own (@itemlabel{L}, or - [L] in
   markdown), as LaTeX's \item[L]: the label replaces the bullet and is
   set flush right against the text, so that the text lines up with
   that of the other items, and a long label sticks out to the left.
   Taken out of the flow, the label leaves the space after it at the
   start of the line, where it is dropped. */
li.lpdoc-labeled {
    list-style: none;
    position: relative;
}
li.lpdoc-labeled > .lpdoc-itemlabel {
    position: absolute;
    right: 100%;
    padding-right: .45em;
    white-space: nowrap;
}

/* An image of class lpdoc-lineart (@image{File}{}{}{lpdoc-lineart}).
   A line art figure (to distinguish it from an image), such as a
   diagram drawn in dark ink for a white page, shows badly on the dark
   theme, so its lightness is inverted and its hues put back, so that
   black ink becomes white while red stays red and blue stays blue. */
html[data-theme='dark'] img.lpdoc-lineart {
    filter: invert(1) hue-rotate(180deg);
}

/* @hfill: a line holding one is made a row by lpdoc.js (layout_hfills),
   its pieces side by side and each @hfill a spacer taking an equal share
   of the free width, as LaTeX's \hfill. If the pieces do not fit, the row
   wraps between them, and a piece too wide for a row wraps within it. */
.lpdoc-hfill-line {
    display: flex;
    flex-wrap: wrap;
    align-items: baseline;
}
.lpdoc-hfill {
    flex: 1 1 0;
    min-width: 1em;
}

/* A centered block (@begin{center} ... @end{center}): its lines and
   images are centered, as in LaTeX, and so are list items, with their
   bullets. Code, runnable code, and the cells of tables keep their
   own alignment. */
.lpdoc-center {
    text-align: center;
}
.lpdoc-center ul,
.lpdoc-center ol {
    list-style-position: inside;
    padding-left: 0;
}
.lpdoc-center pre,
.lpdoc-center td,
.lpdoc-center .lpdoc-runnable-container {
    text-align: left;
}
/* Tables, which are otherwise as wide as the page, are in this case
   as wide as their content and centered (as a tabular in LaTeX's
   center). */
.lpdoc-center table.lpdoc-table {
    width: auto;
    margin-left: auto;
    margin-right: auto;
}

/* Side-by-side columns (@begin{columns} ... @column ... @end{columns}).
   Gives each column a share of the horizontal space, that grows with
   window width.  Columns are aligned at the top, appropriate for
   comparisons of, e.g., code, and they fall back to stacked if there
   is no room for them side by side. */
div.lpdoc-columns {
    display: flex;
    flex-wrap: wrap;
    align-items: flex-start;
    gap: 20px;
    margin-block-start: 0.5em;
    margin-block-end: 0.5em;
}

div.lpdoc-columns > div.lpdoc-column {
    flex-basis: 0;
    min-width: 12em; /* narrower than this and the columns wrap instead */
}

div.lpdoc-twocolumns {
    -moz-column-count: 2;
    -moz-column-gap: 20px;
    -webkit-column-count: 2;
    -webkit-column-gap: 20px;
    column-count: 2;
    column-gap: 20px;
}

.lpdoc-table {
  border-collapse: collapse;
  width: 100%;
}

/* A little room above and below the text of a cell, and at the sides about
   LaTeX's \tabcolsep (half an em): a row is then mostly its text, and tables
   stay compact. */
.lpdoc-table td, .lpdoc-table th {
  border: 1px solid var(--border);
  padding: .2em .5em;
}

.lpdoc-table th {
  border: 1px solid var(--border);
  background: var(--defname-bg);
  text-align: left;
  font-weight: bold;
}

/* --------------------------------------------------------------------------- */
/* Page elements */

div.lpdoc-nav {
    padding: 5px 0px 5px 0px;
    background-color: var(--bg);
}
div.lpdoc-nav ul {
    margin:0;
    padding:0;
    list-style:none;
}
div.lpdoc-nav li {
    display:inline;
    margin:0;
    padding:0;
}

div.lpdoc-nav .header-icon-img {
  height: 18px;
  width: 18px;
  vertical-align: middle;
  margin-right: 10px;
}

div.lpdoc-main {
    color: var(--fg);
    background-color: var(--bg);
    padding: 1px 20px 0px 20px;
    /* padding: 1px 20px 30px 20px; */
    /* border-right: 1px solid #dedede; */ /* right-sidebar */
}

div.lpdoc-sidebar {
    background-color: var(--bg);
    padding:10px 10px 10px 20px;
    font-size: 14px;
    line-height: 1.3em;
}

div.lpdoc-sidebar h2 {
    margin-top: 1ex;
}

div.lpdoc-clearer {
    clear: both;
}

div.lpdoc-footer {
    font-size: 11px;
    /* font-size: 75%; */
    color: var(--fgdim);
    background-color: var(--bg);
    border-top: 1px solid var(--border);
    /* background-color: #f8f8f8; */
    width: 100%;
    padding: 3px 0 3px 0;
    margin-top: 30px;
    text-align: center;
}

div.lpdoc-footer a {
    color: var(--fg);
    text-decoration: underline;
}

h1, h2, h3, h4, h5, h6 {
    font-family: -apple-system,Helvetica,Arial,sans-serif;
    line-height: 1.3em;
    font-weight: 600;
    color: var(--header);
}

/* --------------------------------------------------------------------------- */
/* Page layout */

div.lpdoc-page {
    background-color: var(--bg);
}

/* Document with left sidebar */
.leftbar {}
.leftbar > div.lpdoc-main {
    margin-left: 230px;
}
.leftbar > div.lpdoc-sidebar {
    box-sizing: border-box; /* include padding in width */
    float: left;
    width: 230px;
    height: 100%;
    position: relative;
}

/* Document with right sidebar */
.rightbar {}
.rightbar > div.lpdoc-main {
    margin-right: 230px;
}
.rightbar > div.lpdoc-sidebar {
    box-sizing: border-box; /* include padding in width */
    float: right;
    width: 230px;
    height: 100%;
    position: relative;
}

/* Document with left sidebar */
.fixleftbar {}
.fixleftbar > div.lpdoc-main {
    margin-left: 230px;
}
.fixleftbar > div.lpdoc-sidebar {
    box-sizing: border-box; /* include padding in width */
    float: left;
    width: 230px;
    height: 100%;
    position: fixed;
    overflow-y: auto;
    top: 0;
    bottom: 0;
    border-right: 1px solid var(--border);
}

/* Document with right sidebar */
.fixrightbar {}
.fixrightbar > div.lpdoc-main {
    margin-right: 230px;
}
.fixrightbar > div.lpdoc-sidebar {
    box-sizing: border-box; /* include padding in width */
    float: fixright;
    width: 230px;
    height: 100%;
    position: fixed;
    overflow-y: auto;
    top: 0;
    bottom: 0;
    border-left: 1px solid var(--border);
}

hr {
    border: none;
    border-top: 1px solid var(--border);
}
/* A rule in the text (@hrule) is meant to be seen: about 2.8:1 against
   the page in both themes, where --border, the colour of the faintest
   dividers (as those of the sidebar), is 1.2:1 and 1.3:1 */
.lpdoc-main hr {
    border-top-color: var(--rule);
}

/* --------------------------------------------------------------------------- */
/* Links */

div.lpdoc-sidebar a:link { color: var(--sidebar-link); text-decoration: none; }
div.lpdoc-sidebar a:visited { color: var(--sidebar-link); text-decoration: none; }
div.lpdoc-sidebar a:hover { color: var(--link-fg); text-decoration: none; }

a.lpdoc-missing:link { color: #aa0000; text-decoration: none; }
a.lpdoc-missing:visited { color: #aa0000; text-decoration: none; }
a.lpdoc-missing:hover { color: #aa0000; text-decoration: underline; }
a.lpdoc-missing:active { color: #FA0000; text-decoration: underline; }

a.lpdoc-idx-anchor:link { color: var(--link-fg); text-decoration: none; }
a.lpdoc-idx-anchor:visited { color: var(--link-fg); text-decoration: none; }
a.lpdoc-idx-anchor:hover { color: var(--link-fg); text-decoration: underline; }
a.lpdoc-idx-anchor:active { color: var(--link-fg); text-decoration: underline; }

div.lpdoc-defname a.lpdoc-idx-anchor:link { color: var(--fg); text-decoration: none; }
div.lpdoc-defname a.lpdoc-idx-anchor:visited { color: var(--fg); text-decoration: none; }
div.lpdoc-defname a.lpdoc-idx-anchor:hover { color: var(--fg); text-decoration: underline; }
div.lpdoc-defname a.lpdoc-idx-anchor:active { color: var(--fg); text-decoration: underline; }

a:link { color: var(--link-fg); text-decoration: none; }
a:visited { color: var(--link-fg); text-decoration: none; }
a:hover { color: var(--link-fg); text-decoration: underline; }
a:active { color: var(--link-fg); text-decoration: underline; }

/* --------------------------------------------------------------------------- */
/* Navigation buttons (special links) */

.lpdoc-navbutton,
.lpdoc-navbutton-disabled {
    font-size: 20px;
    border-radius: 2px;
    padding: 2px 8px 2px 8px;
    margin-left: 1px;
    margin-right: 1px;
}

.lpdoc-navbutton { color: var(--link-fg); }
a.lpdoc-navbutton:link { color: var(--link-fg); text-decoration: none; }
a.lpdoc-navbutton:visited { color: var(--link-fg); text-decoration: none; }
a.lpdoc-navbutton:hover { color: var(--link-fg); text-decoration: none; }
a.lpdoc-navbutton:active { color: #FAA700; text-decoration: none; }

.lpdoc-navbutton-disabled { color: var(--border); }

/* --------------------------------------------------------------------------- */
/* Toggleable sidebar (for small screens) */

div#sidebar {
    display: block;
}

a#sidebar-toggle-button {
    display:none;
}

/* --------------------------------------------------------------------------- */
/* Menu at sidebar */

div.lpdoc-sidebar h2 {
    font-size: 100%;
}

div.lpdoc-sidebar p {
    margin-left: 0px;
}

/* ul for sectpath in sidebar */
div.lpdoc-sidebar ul.lpdoc-itemize-sectpath {
    margin-left: 0px;
    list-style-type: none;
    color: var(--sidebar-link);
    padding-left: 0px;
    margin: 0px;
}

div.lpdoc-sidebar ul {
    margin-left: 0px;
    list-style-type: circle;
    color: #9cadd3;
    padding-left: 16px;
    margin: 0px;
}

div.lpdoc-sidebar li {
    /* list-style-type: circle; */
    padding-left: 0px;
    /* margin: 0px; */
    /* (tighter when names are split into several lines) */
    line-height: 1.0;
    margin: 6px 0px 6px 0px;
}

/* --------------------------------------------------------------------------- */
/* Cover */

div.lpdoc-cover-address {
    line-height:1.3em;
    font-size: 11px;
    float:right;
    /* padding: 16px; */
    padding-left: 16px;
    color: var(--fgdim);
}

div.lpdoc-cover-authors {
    font-size: 11px;
    line-height: 1.3em;
    /* padding: 16px; */
    float:right;
    text-align:right;
    color: var(--fgdim);
}

div.lpdoc-cover-logo {
    float: right;
}

div.lpdoc-cover-title {
    /* padding: 16px; */
    margin: 0px;
    margin-bottom: 16px;
    background-color: var(--bg);
    color: var(--header);
}

div.lpdoc-cover-subtitle-extra {
    font-size: 11px;
    line-height: 1.3em;
    /* padding: 16px; */
    border-radius: 8px;
    color: var(--fgdim);
}

h1.lpdoc-cover-h1 {
    margin-bottom:0px;
    font-size: 40px;
}

/* --------------------------------------------------------------------------- */
/* Ciao syntax highlight (htmlfontify) */

html {
    --face-sectioning: #000080;
    --face-funexp-atom: #6b8e23;
    --face-type-assrt: #0000cd;
    --face-prop-assrt: #0000ff;
    --face-entry-assrt: #a52a2a;
    --face-trust-assrt: #ff7f50;
    --face-false-assrt: #ff0000;
    --face-true-assrt: #228b22;
    --face-check-assrt: #000080;
    --face-checked-assrt: #006400;
    --face-lpdoc-command: #4169e1;
    --face-lpdoc-verbatim: #000080;
    --face-lpdoc-include: #000080;
    --face-concurrency-op: #ff7f50;
    --face-prompt: #ff7f50;
    --face-variable: #a0522d;
    --face-string: #bc8f8f;
    --face-lpdoc-comment: #000080;
    --face-lpdoc-bug-comment: #ff0000;
    --face-clauseheadname: #0000ff;
    --face-user-directive: #000080;
    --face-library-directive: #000080;
    --face-predicate-directive: #4169e1;
    --face-builtin-directive: #0000ff;
    --face-quoted-atom: #666666;
    --face-module-directive: #000080;
    --face-comment: #b22222;
    --face-cut: #4169e1;
    --face-error-mess: #ff0000;
    --face-warning-mess: #a52a2a;
    --face-other-mess: #a52a2a;
    --face-no-answer: #b8860b;
    --face-yes-answer: #228b22;
    --face-answer-var: #a020f0;
    --face-answer-val: #0000ff;

    --face-debug-call: #5f42f4;
    --face-debug-call-bg: #5f42f440;
    --face-debug-exit: #7dd120;
    --face-debug-exit-bg: #7dd12040;
    --face-debug-fail: #b22222;
    --face-debug-fail-bg: #b2222240;
    --face-debug-redo: #ffa500;
    --face-debug-redo-bg: #ffa50040;
    --face-debug-expansion: #ffff00;
    --face-debug-expansion-bg: #ffff0020;
    --face-debug-breakpoint: #ff0000;
}

html[data-theme='dark'] {
    --face-sectioning: #ffec8b;
    --face-funexp-atom: #b3ee3a;
    --face-type-assrt: #1e90ff;
    --face-prop-assrt: #1e90ff;
    --face-entry-assrt: #ff8c69;
    --face-trust-assrt: #ff7f50;
    --face-false-assrt: #ff0000;
    --face-true-assrt: #32cd32;
    --face-checked-assrt: #90ee90;
    --face-check-assrt: #1e90ff;
    --face-cut: #6495ed;
    --face-concurrency-op: #ff7f50;
    --face-prompt: #ff7f50;
    --face-variable: #eedd82;
    --face-string: #ffa07a;
    --face-lpdoc-command: #c6e2ff;
    --face-lpdoc-bug-comment: #ff0000;
    --face-lpdoc-comment: #9fb6cd;
    --face-clauseheadname: #87cefa;
    --face-user-directive: #1e90ff;
    --face-library-directive: #1e90ff;
    --face-predicate-directive: #1e90ff;
    --face-builtin-directive: #87cefa;
    --face-quoted-atom: #e5e5e5;
    --face-module-directive: #9f79ee;
    --face-comment: #6c7b8b;
    --face-script-header: #32cd32;
    --face-error-mess: #ff0000;
    --face-warning-mess: #ff8c69;
    --face-other-mess: #ff8c69;
    --face-no-answer: #eedd82;
    --face-yes-answer: #32cd32;
    --face-answer-var: #00ffff;
    --face-answer-val: #87cefa;

    --face-debug-call: #2793fa;
    --face-debug-call-bg: #2793fa40;
    --face-debug-exit: #7dd120;
    --face-debug-exit-bg: #7dd12040;
    --face-debug-fail: #b22222;
    --face-debug-fail-bg: #b2222240;
    --face-debug-redo: #ffa500;
    --face-debug-redo-bg: #ffa50040;
    --face-debug-expansion: #ffff00;
    --face-debug-expansion-bg: #ffff0020;
    --face-debug-breakpoint: #ff0000;
    /*--face-debug-call: #0000cd80;
    --face-debug-exit: #556b2f80;
    --face-debug-fail: #b2222280;
    --face-debug-redo: #ffa50080;
    --face-debug-expansion: #ffff0080;
    --face-debug-breakpoint: #ff000080;*/
}

span.ciao-face-sectioning-5-face   { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; text-decoration: none; }
span.ciao-face-sectioning-5-face a { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; text-decoration: underline; }
span.ciao-face-sectioning-4-face   { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 15pt; text-decoration: none; }
span.ciao-face-sectioning-4-face a { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 15pt; text-decoration: underline; }
span.ciao-face-sectioning-3-face   { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 18pt; text-decoration: none; }
span.ciao-face-sectioning-3-face a { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 18pt; text-decoration: underline; }
span.ciao-face-sectioning-2-face   { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 20pt; text-decoration: none; }
span.ciao-face-sectioning-2-face a { color: var(--face-sectioning); font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 20pt; text-decoration: underline; }
span.ciao-face-funexp-atom   { color: var(--face-funexp-atom); font-weight: 500; text-decoration: none; }
span.ciao-face-funexp-atom a { color: var(--face-funexp-atom); font-weight: 500; text-decoration: underline; }
span.ciao-face-type-assrt   { color: var(--face-type-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-type-assrt a { color: var(--face-type-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-prop-assrt   { color: var(--face-prop-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-prop-assrt a { color: var(--face-prop-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-entry-assrt   { color: var(--face-entry-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-entry-assrt a { color: var(--face-entry-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-trust-assrt   { color: var(--face-trust-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-trust-assrt a { color: var(--face-trust-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-false-assrt   { color: var(--face-false-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-false-assrt a { color: var(--face-false-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-true-assrt   { color: var(--face-true-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-true-assrt a { color: var(--face-true-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-check-assrt   { color: var(--face-check-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-check-assrt a { color: var(--face-check-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-checked-assrt   { color: var(--face-checked-assrt); font-weight: 700; text-decoration: none; }
span.ciao-face-checked-assrt a { color: var(--face-checked-assrt); font-weight: 700; text-decoration: underline; }
span.ciao-face-lpdoc-command   { color: var(--face-lpdoc-command); font-weight: 500; text-decoration: none; }
span.ciao-face-lpdoc-command a { color: var(--face-lpdoc-command); font-weight: 500; text-decoration: underline; }
span.ciao-face-lpdoc-verbatim   { color: var(--face-lpdoc-verbatim); font-weight: 700; text-decoration: none; }
span.ciao-face-lpdoc-verbatim a { color: var(--face-lpdoc-verbatim); font-weight: 700; text-decoration: underline; }
span.ciao-face-lpdoc-include   { color: var(--face-lpdoc-include); font-weight: 700; text-decoration: none; }
span.ciao-face-lpdoc-include a { color: var(--face-lpdoc-include); font-weight: 700; text-decoration: underline; }
span.ciao-face-concurrency-op   { color: var(--face-concurrency-op); font-weight: 700; text-decoration: none; }
span.ciao-face-concurrency-op a { color: var(--face-concurrency-op); font-weight: 700; text-decoration: underline; }
span.ciao-face-prompt   { color: var(--face-prompt); font-weight: 700; text-decoration: none; }
span.ciao-face-prompt a { color: var(--face-prompt); font-weight: 700; text-decoration: underline; }
span.ciao-face-variable   { color: var(--face-variable); font-weight: 500; text-decoration: none; }
span.ciao-face-variable a { color: var(--face-variable); font-weight: 500; text-decoration: underline; }
span.ciao-face-string   { color: var(--face-string); font-weight: 500; text-decoration: none; }
span.ciao-face-string a { color: var(--face-string); font-weight: 500; text-decoration: underline; }
span.ciao-face-lpdoc-comment   { color: var(--face-lpdoc-comment); font-weight: 500; text-decoration: none; }
span.ciao-face-lpdoc-comment a { color: var(--face-lpdoc-comment); font-weight: 500; text-decoration: underline; }
span.ciao-face-lpdoc-bug-comment   { color: var(--face-lpdoc-bug-comment); font-weight: 700; text-decoration: none; }
span.ciao-face-lpdoc-bug-comment a { color: var(--face-lpdoc-bug-comment); font-weight: 700; text-decoration: underline; }
span.ciao-face-clauseheadname   { color: var(--face-clauseheadname); font-weight: 500; text-decoration: none; }
span.ciao-face-clauseheadname a { color: var(--face-clauseheadname); font-weight: 500; text-decoration: underline; }
span.ciao-face-user-directive   { color: var(--face-user-directive); font-weight: 500; text-decoration: none; }
span.ciao-face-user-directive a { color: var(--face-user-directive); font-weight: 500; text-decoration: underline; }
span.ciao-face-library-directive   { color: var(--face-library-directive); font-weight: 700; text-decoration: none; }
span.ciao-face-library-directive a { color: var(--face-library-directive); font-weight: 700; text-decoration: underline; }
span.ciao-face-predicate-directive   { color: var(--face-predicate-directive); font-weight: 500; text-decoration: none; }
span.ciao-face-predicate-directive a { color: var(--face-predicate-directive); font-weight: 500; text-decoration: underline; }
span.ciao-face-builtin-directive   { color: var(--face-builtin-directive); font-weight: 700; text-decoration: none; }
span.ciao-face-builtin-directive a { color: var(--face-builtin-directive); font-weight: 700; text-decoration: underline; }
span.ciao-face-quoted-atom   { color: var(--face-quoted-atom); font-weight: 500; text-decoration: none; }
span.ciao-face-quoted-atom a { color: var(--face-quoted-atom); font-weight: 500; text-decoration: underline; }
span.ciao-face-module-directive   { color: var(--face-module-directive); font-weight: 700; text-decoration: none; }
span.ciao-face-module-directive a { color: var(--face-module-directive); font-weight: 700; text-decoration: underline; }
span.ciao-face-comment   { color: var(--face-comment); font-weight: 500; text-decoration: none; }
span.ciao-face-comment a { color: var(--face-comment); font-weight: 500; text-decoration: underline; }
span.ciao-face-cut   { color: var(--face-cut); font-weight: 500; text-decoration: none; }
span.ciao-face-cut a { color: var(--face-cut); font-weight: 500; text-decoration: underline; }
span.ciao-face-error-mess   { color: var(--face-error-mess); font-weight: 700; text-decoration: none; }
span.ciao-face-error-mess a { color: var(--face-error-mess); font-weight: 700; text-decoration: underline; }
span.ciao-face-warning-mess { color: var(--face-warning-mess); font-weight: 700; text-decoration: none; }
span.ciao-face-warning-mess a { color: var(--face-warning-mess); font-weight: 700; text-decoration: underline; }
span.ciao-face-other-mess { color: var(--face-other-mess); font-weight: 500; text-decoration: none; }
span.ciao-face-other-mess a { color: var(--face-other-mess); font-weight: 500; text-decoration: underline; }
span.ciao-face-no-answer { color: var(--face-no-answer); font-weight: 700; text-decoration: none; }
span.ciao-face-no-answer a { color: var(--face-no-answer); font-weight: 700; text-decoration: underline; }
span.ciao-face-yes-answer { color: var(--face-yes-answer); font-weight: 700; text-decoration: none; }
span.ciao-face-yes-answer a { color: var(--face-yes-answer); font-weight: 700; text-decoration: underline; }
ciao-face-answer-var { color: var(--face-answer-var); font-weight: 700; text-decoration: none; }
ciao-face-answer-var a { color: var(--face-answer-var); font-weight: 700; text-decoration: underline; }
ciao-face-answer-val { color: var(--face-answer-val); font-weight: 700; text-decoration: none; }
ciao-face-answer-val a { color: var(--face-answer-val); font-weight: 700; text-decoration: underline; }

.ciao-face-debug-call { box-shadow: inset 0px 0px 0px 1px var(--face-debug-call); background: var(--face-debug-call-bg); }
.ciao-face-debug-call-bg { background: var(--face-debug-call-bg); }
.ciao-face-debug-exit { box-shadow: inset 0px 0px 0px 1px var(--face-debug-exit); background: var(--face-debug-exit-bg); }
.ciao-face-debug-exit-bg { background: var(--face-debug-exit-bg); }
.ciao-face-debug-fail { box-shadow: inset 0px 0px 0px 1px var(--face-debug-fail); background: var(--face-debug-fail-bg); }
.ciao-face-debug-fail-bg { background: var(--face-debug-fail-bg); }
.ciao-face-debug-redo { box-shadow: inset 0px 0px 0px 1px var(--face-debug-redo); background: var(--face-debug-redo-bg); }
.ciao-face-debug-redo-bg { background: var(--face-debug-redo-bg); }
.ciao-face-debug-expansion { box-shadow: inset 0px 0px 0px 1px var(--face-debug-expansion); background: var(--face-debug-expansion-bg); }
.ciao-face-debug-expansion-bg { background: var(--face-debug-expansion-bg); }
.ciao-face-debug-breakpoint { background: var(--face-debug-breakpoint); }

/* Other languages */
span.constant   { color: #008b8b; font-weight: 500; text-decoration: none; }
span.constant a { color: #008b8b; font-weight: 500; text-decoration: underline; }
span.negation-char   { font-weight: 500; color: #000000; text-decoration: none; }
span.negation-char a { font-weight: 500; color: #000000; text-decoration: underline; }
span.variable-name   { color: #a0522d; font-weight: 500; text-decoration: none; }
span.variable-name a { color: #a0522d; font-weight: 500; text-decoration: underline; }
span.type   { color: #228b22; font-weight: 500; text-decoration: none; }
span.type a { color: #228b22; font-weight: 500; text-decoration: underline; }
span.hc-tab   { background: #000000; font-weight: 500; color: #000000; text-decoration: none; }
span.hc-tab a { background: #000000; font-weight: 500; color: #000000; text-decoration: underline; }
span.hc-trailing-whitespace   { background: #000000; font-weight: 500; color: #000000; text-decoration: none; }
span.hc-trailing-whitespace a { background: #000000; font-weight: 500; color: #000000; text-decoration: underline; }
span.function-name   { color: #0000ff; font-weight: 500; text-decoration: none; }
span.function-name a { color: #0000ff; font-weight: 500; text-decoration: underline; }
span.keyword   { color: #a020f0; font-weight: 500; text-decoration: none; }
span.keyword a { color: #a020f0; font-weight: 500; text-decoration: underline; }
span.string   { color: #8b2252; font-weight: 500; text-decoration: none; }
span.string a { color: #8b2252; font-weight: 500; text-decoration: underline; }
span.preprocessor   { color: #483d8b; font-weight: 500; text-decoration: none; }
span.preprocessor a { color: #483d8b; font-weight: 500; text-decoration: underline; }
span.comment   { color: #b22222; font-weight: 500; text-decoration: none; }
span.comment a { color: #b22222; font-weight: 500; text-decoration: underline; }
span.comment-delimiter   { color: #b22222; font-weight: 500; text-decoration: none; }
span.comment-delimiter a { color: #b22222; font-weight: 500; text-decoration: underline; }
span.sh-quoted-exec   { color: #ff00ff; font-weight: 500; text-decoration: none; }
span.sh-quoted-exec a { color: #ff00ff; font-weight: 500; text-decoration: underline; }

/* --------------------------------------------------------------------------- */
/* Search */

#search-input {
    font-family: SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;
    font-size: 14px;
    line-height: normal;
    padding: 8px;
    color: var(--codeblock-fg);
    background-color: var(--codeblock-bg);
    border: 1px solid var(--codeblock-border);
    border-radius: 3px;
    width: 80%;
    box-sizing: border-box;
}
#search-input:focus {
    outline: none;
}

/* --------------------------------------------------------------------------- */
/* LPdoc dynamic (runnable, etc.) code blocks (see ciao_playground) */

.lpdoc-codeblock-dynamic { display: none; } /* (hidden by default) */

.lpdoc-runnable-container {
    position: relative;
    margin-top: 1em;
    margin-bottom: 1em;
}

/* .lpdoc-runnable-container details {
    font-size: 12px;
    padding: .25em .5em 0 .5em;
}

.lpdoc-runnable-container summary {
    margin: -.25em -.5em 0 -.5em;
    padding: .25em .5em .25em .5em;
    user-select: none;
    color: var(--link-fg);
}

.lpdoc-runnable-container details[open] {
    padding: .25em .5em .25em .5em;
}*/

.lpdoc-runnable-help {
    color: var(--sidebar-link);
    border: 1px solid var(--note-bg);
    border-radius: 5px;
    background: var(--note-bg);
    font-size: 12px;
    cursor: pointer;
}

/* The solution of an exercise, shown on demand below it */
.lpdoc-runnable-solution-bar {
    display: flex;
    gap: 8px;
}
.lpdoc-runnable-solution .lpdoc-runnable-editor-container {
    margin-top: 6px;
}

.lpdoc-runnable-statusmark {
}
.lpdoc-runnable-status-failed {
    color: #ff6262;
}
.lpdoc-runnable-status-checked {
    color: #6eb88c;
}
.lpdoc-runnable-status-unknown {
    color: #ffa162;
}
.lpdoc-runnable-status-load {
  /* inherits fgdim */
}
.comint-echo {
    font-size: 14px;
    font-family: -apple-system,Helvetica,Arial,sans-serif;
    font-weight: bold;
    line-height: normal;
    right: 5px;
    top: 5px;
    padding: 2px 4px 2px 4px;
    border-radius: 3px;
}
.comint-echo-running {
    color: var(--link-fg);
}
.comint-echo-error {
    color: red;
}
.comint-echo-hidden {
    display: none
}

.lpdoc-runnable-comint {
    display: none
}
.lpdoc-runnable-preview {
    display: none
}

.lpdoc-runnable-buttons {
    position: absolute;
    z-index: 100;
    right: 5px;
    top: 5px;
    color: var(--fgdim);
    cursor: pointer;
}

.lpdoc-runnable-button {
    color: var(--fgdim);
    margin-right: 5px;
    padding: 0;
    font-size: 14px;
    cursor: pointer;
    background: transparent;
    border: 0px;
    /* border: 1px solid var(--fgdim);
    border-radius: 3px; */
    /* width: 20px; */
    height: 20px;
}

/* While a cell runs (see set_busy in ciao_playground.js): a spinner in
   place of the mark of its run button, and, if its output is hidden, its
   control line (what runs, and Abort) over the bottom of the cell */
.lpdoc-runnable-button.lpdoc-runnable-busy {
    position: relative;
}
.lpdoc-runnable-button.lpdoc-runnable-busy > * {
    visibility: hidden;
}
.lpdoc-runnable-button.lpdoc-runnable-busy::after {
    content: "";
    position: absolute;
    left: 50%;
    top: 50%;
    width: 10px;
    height: 10px;
    margin: -7px 0 0 -7px;
    border: 2px solid currentColor;
    border-right-color: transparent;
    border-radius: 50%;
    animation: lpdoc-spin 0.8s linear infinite;
}
@keyframes lpdoc-spin {
    to { transform: rotate(360deg); }
}
.lpdoc-runnable-running > .comint-echo-hidden {
    display: block;
    position: absolute;
    z-index: 100;
    right: 5px;
    bottom: 5px;
}
.lpdoc-runnable-running > .comint-echo-hidden .comint-editor-container {
    display: none;
}
.lpdoc-runnable-running > .comint-echo-hidden .comint-control {
    width: auto;
    margin-top: 0;
    padding: 4px 4px 4px 8px;
    border: 1px solid var(--codeblock-border);
    border-radius: 6px;
    background: var(--bg);
}
.lpdoc-runnable-running > .comint-echo-hidden .comint-echo {
    margin-right: 8px;
}

/* --------------------------------------------------------------------------- */
/* UI - Dropdown menus */

/* dropdown buttons */
.dropdown-btn {
  font-family: -apple-system,Helvetica,Arial,sans-serif;
  font-size: 17px;
  font-weight: 500;
  color: var(--sidebar-link);
  background: none;
  border: none;
  cursor: pointer;
  padding: 0px;
}

.dropdown {
  position: relative;
  display: inline-block;
}

.dropdown-content {
  display: none;
  position: absolute;
  padding: 5px 5px;
  background-color: var(--dropdown-bg);
  border-radius: 6px;
  /* min-width: 160px; */
  width: max-content;
  box-shadow: 0px 8px 16px 0px rgba(0,0,0,0.2);
  z-index: 1;
  /* overflow: hidden; */
  overflow-x: hidden;
  overflow-y: auto;
  max-height: 70vh;
}

div.dropdown-content a {
  font-family: -apple-system,Helvetica,Arial,sans-serif;
  font-size: 15px;
  color: var(--fg);
  padding: 5px 10px;
  text-align: justify;
  text-decoration: none;
  display: block;
  cursor: pointer;
}

div.dropdown-content a:hover {
  text-decoration: none;
  background-color: var(--fg);
  color: var(--dropdown-bg);
  border-radius: 3px;
}

.dropdown-mark {
  display: inline-block;
  width: 14px;
}

/* A submenu (see DropdownButton): its items show below it, indented, when
   it is unfolded */
div.dropdown-content a.dropdown-parent::after {
  content: " \25B8";
}
div.dropdown-content a.dropdown-parent.dropdown-unfolded::after {
  content: " \25BE";
}
div.dropdown-content a.dropdown-subitem {
  display: none;
  padding-left: 2em;
}
div.dropdown-content a.dropdown-subitem.dropdown-subshow {
  display: block;
}

.show {
  display: block;
}

/* --------------------------------------------------------------------------- */
/* UI - Menu bars */

/* Top left menu */
.main-menu {
  flex: 0 1 auto;
  font-family: -apple-system,Helvetica,Arial,sans-serif;
  font-size: 15px;
  width: 100%;
  padding-left: 0px;
  padding-right: 0px;
  padding-bottom: 8px;
  display: flex;
}

.main-menu label {
  display: block;
  position: relative;
  color: var(--button-color);
  border: 1px solid var(--button-border);
  border-radius: 6px;
  background: var(--button-bg);
  /* background: linear-gradient(90deg, rgba(239, 239, 239, 1) 0%, rgba(233, 233, 237, 1) 35%, rgba(241, 243, 244, 1) 100%); */
  /* height: 21px; */
  width: 50px;
  margin-right: 5px;
  display: flex;
  align-items: center;
  justify-content: center;
}

.main-menu label:hover {
  border: 1px solid var(--button-border-hover);
  cursor: pointer;
}

.main-menu .header-icon-img {
  height: 20px;
  width: 20px;
  margin-top: 0px;
}

.main-menu .header-icon-img:hover {
  transform: scale(1.0);
}

.menu-button {
  font-family: -apple-system,Helvetica,Arial,sans-serif;
  font-size: 15px;
  color: var(--button-color);
  border: 1px solid var(--button-border);
  border-radius: 6px;
  padding: 4px 8px 4px 8px;
  background: var(--button-bg);
  margin-right: 5px;
  /* background: linear-gradient(90deg, rgba(239, 239, 239, 1) 0%, rgba(233, 233, 237, 1) 35%, rgba(241, 243, 244, 1) 100%); */
  /*    height: 23px; */
}
.menu-button:hover {
  border: 1px solid var(--button-border-hover);
  cursor: pointer;
}

.right-menu {
  margin-left: auto;
  margin-right: 0px;
  display: flex;
}
.right-menu .menu-button {
  margin-right: 0px;
  margin-left: 5px;
}

/* --------------------------------------------------------------------------- */
/* Runnable code (editor) */

.lpdoc-runnable-editor-container,
.lpdoc-runnable-container .comint-editor-container {
  border: 1px solid var(--codeblock-border);
  border-radius: 3px;
  padding-top: 8px;
  padding-bottom: 8px;
  background: var(--codeblock-bg);
}

.monaco-editor .scroll-decoration { /* (does not look nice in our setting) */
  box-shadow: none !important;
}

/* --------------------------------------------------------------------------- */
/* Comint (command-interpreter-in-a-buffer ala emacs) */

.comint-container {
  width: 100%;
  height: 100%;
  display: flex;
  flex-flow: column;
}
.comint-editor-container {
  flex: 1 1 auto;
  border: 1px solid var(--codeblock-border);
  border-radius: 6px;
  overflow: hidden;
}
/* control bar for toplevel query buttons */
.comint-control {
  width: 100%;
  flex: 0 1 26px;
  margin-top: 8px; /* (only top margin to separate from toplevelEd) */
}

/* avoid scrollback (use instead of 'hidden'; solution from https://github.com/microsoft/monaco-editor/issues/1588) */
/*
.editor-container .monaco-editor { overflow: unset; } 
.comint-container .monaco-editor { overflow: unset; } 
*/

.comint-button {
  font-family: -apple-system,Helvetica,Arial,sans-serif;
  font-size: 14px;
  color: var(--button-color);
  border: 1px solid var(--button-border);
  border-radius: 6px;
  padding: 4px 8px 4px 8px;
  background: var(--button-bg);
  display: none;
  margin-right: 5px;
}

.comint-button:hover {
  border: 1px solid var(--button-border-hover);
  cursor: pointer;
}

.comint-button-abort {
  /* width: 115px; */
  float: right;
  /* transition: all 0.3s ease; */
  opacity: 1;
  animation-name: fadeInOpacity;
  animation-iteration-count: 1;
  animation-timing-function: ease-in;
  animation-duration: 0.5s;
  margin-right: 0px;
}

@keyframes fadeInOpacity {
    0% { opacity: 0; }
    100% { opacity: 1; }
}

/* --------------------------------------------------------------------------- */
/* Playgroung editing and toplevel */

/* TODO: move to ciao_playground.css? */

.playground {
  overflow: hidden;
  margin: 0px;
  padding: 0px;
  flex: 1 1 auto;
  /*height: calc(100% - 35px);*/
  width: 100%;
  /* box-sizing: border-box; */
}

/* (see split.js documentation) */
.split-vert {
}
.split-horiz {
  display: flex;
  flex-direction: row;
}
.gutter.gutter-vertical {
  cursor: row-resize;
}
.gutter.gutter-horizontal {
  cursor: col-resize;
}

.editor-container {
  border: 1px solid var(--codeblock-border);
  overflow: hidden;
  border-radius: 6px;
}

.preview-container {
  width: calc(100% - 2px);
  height: calc(100% - 2px);
  border: 1px solid var(--border);
  overflow: hidden;
  border-radius: 6px;
  /* some default background */
  background-image:
    repeating-linear-gradient(45deg, var(--border) 25%, transparent 25%, transparent 75%, var(--border) 75%, var(--border)),
    repeating-linear-gradient(45deg, var(--border) 25%, var(--bg) 25%, var(--bg) 75%, var(--border) 75%, var(--border));
  background-position: 0 0, 8px 8px;
  background-size: 16px 16px;
}

/* Minor style adjustements when using the preview container */

.preview-container h1.lpdoc-cover-h1 {
  margin:0px;
}

.preview-container div.lpdoc-nav .header-icon-img {
  margin-left: 10px;
  margin-right: 0px;
}

/* --------------------------------------------------------------------------- */
/* Mobile-friendly */

@media (max-width: 700px) {
    /* Reset sidebar position */
    .leftbar > div.lpdoc-main { margin-left: 0; }
    .rightbar > div.lpdoc-main { margin-right: 0; }
    .leftbar > div.lpdoc-sidebar,
    .rightbar > div.lpdoc-sidebar {
	float: none;
	width: auto;
	position: relative;
    }

    .fixleftbar > div.lpdoc-main { margin-left: 0; }
    .fixrightbar > div.lpdoc-main { margin-right: 0; }
    .fixleftbar > div.lpdoc-sidebar,
    .fixrightbar > div.lpdoc-sidebar {
	float: none;
	width: auto;
	position: relative;
    }

    div.lpdoc-nav {
	padding-right: 20px; /* some space for toggle button */
    }
    a#sidebar-toggle-button {
	z-index: 1;
	display: block;
	position: absolute;
	right: 0;
	top: 0;
	padding:7px 10px 7px 10px;
    }
    div#sidebar {
	display: none;
    }
    div#sidebar.sidebar-toggled {
	display: block;
	border-bottom: 1px solid var(--fgdim);
	font-size: 16px;
	z-index: 0;
    }
}

@media (max-width: 700px) {
  .right-header {
    margin-top: 10px;
  }
  .main-menu .header-icon-img {
    margin-top: 0px;
  }
  .menu-button {
    font-size: 14px;
  }
  .main-menu {
    font-size: 14px;
  }
}

/* --------------------------------------------------------------------------- */
/* Style for slide mode */

/* Reset sidebar position */
.lpdoc-slide-mode .leftbar > div.lpdoc-main,
.lpdoc-slide-mode .fixleftbar > div.lpdoc-main { margin-left: 0; }
.lpdoc-slide-mode .rightbar > div.lpdoc-main,
.lpdoc-slide-mode .fixrightbar > div.lpdoc-main { margin-right: 0; }

.lpdoc-slide-mode a#sidebar-toggle-button,
.lpdoc-slide-mode div#sidebar,
.lpdoc-slide-mode div#sidebar.sidebar-toggled,
.lpdoc-slide-mode .lpdoc-sidebar,
.lpdoc-slide-mode .lpdoc-footer {
  display: none;
}

.lpdoc-slide-mode p {
  margin-block-start: 0.4em;
  margin-block-end: 0.4em;
}

/* Lists in slides are spaced as LaTeX slides space them (xdvislides
   keeps the list parameters of size11.clo for its \LARGE text, measured
   in a PDF deck: 30.9pt between items, 22.5pt between lines, for 17.28pt
   type): items half a line further apart than the lines within an item,
   those of a nested list a fifth of a line, and a nested list half a
   line from the text before and after it. A list at the top keeps the
   1em around it that the browser gives it. Elsewhere lists stay compact,
   as usual in html. */
.lpdoc-slide-mode .lpdoc-slide li + li {
  margin-top: 0.5em;
}
.lpdoc-slide-mode .lpdoc-slide li li + li {
  margin-top: 0.2em;
}
.lpdoc-slide-mode .lpdoc-slide li > ul,
.lpdoc-slide-mode .lpdoc-slide li > ol {
  margin-top: 0.5em;
  margin-bottom: 0.5em;
}

/* And indented as LaTeX slides indent them: \leftmargini .. iv are
   2.5em, 2.2em, 1.87em and 1.7em of the class's normal size (11pt), so
   1.58em, 1.39em, 1.18em and 1.07em of the \LARGE text of the slides
   (measured in a PDF deck: an item's text 27.3pt in from the margin, a
   sub-item's 24pt in from that, for 17.28pt type), where the browser
   gives every level 40px.  Under :where(), so that lists with a style
   of their own (in a cartouche, centered, plain) keep it. */
:where(.lpdoc-slide-mode .lpdoc-slide) :is(ul, ol) {
  padding-left: 1.58em;
}
:where(.lpdoc-slide-mode .lpdoc-slide) :is(ul, ol) :is(ul, ol) {
  padding-left: 1.39em;
}
:where(.lpdoc-slide-mode .lpdoc-slide) :is(ul, ol) :is(ul, ol) :is(ul, ol) {
  padding-left: 1.18em;
}
:where(.lpdoc-slide-mode .lpdoc-slide) :is(ul, ol) :is(ul, ol) :is(ul, ol) :is(ul, ol) {
  padding-left: 1.07em;
}

.lpdoc-slide-mode .lpdoc-slide {
  width: calc(100% - 64px);
  height: calc(100% - 32px);
  padding: 16px 32px 16px 32px;
}

.lpdoc-slide-mode img {
  vertical-align: middle;
  max-width: 700px;
}

.lpdoc-slide-mode body,
.lpdoc-slide-mode html {
  height: 100%;
}

.lpdoc-slide-mode h1.lpdoc-cover-h1 {
  text-align:center;
}

/* this will act as slide container */
.lpdoc-slide-mode .lpdoc-main {
  /* 16:9 ratio */
  width: 800px;
  min-height: 500px; /* (do not fix height, allow vertical scrollbar) */
  position: relative;
  padding: 0px;
  /* zoom: ... */ /* calculated dynamically */
}

/* Scrollbar for slideshows (see lpdoc.js for details) */
.lpdoc-slide-scroll {
  scrollbar-width: thin;
  /* NOTE: we'd really want overlay scrollbars where we can see through
   the scrollbar track, but this is not supported directly in CSS */
  overflow-x: hidden;
}

/* A non-active slide (hidden) */
.lpdoc-slide-mode .lpdoc-slide-hide {
  display: none;
}

/* The marker left by @pause. Just marks where one reveal step ends and
   next begins; never shown. */
.lpdoc-pause {
  display: none;
}

/* A reveal step that has not been reached yet, in slide mode. Hidden by
   visibility rather than display, so that the rest of the slide does not
   move as the steps appear. Outside slide mode nothing is hidden, so a
   printed or scrolled document shows every step. */
.lpdoc-slide-mode .lpdoc-step-hidden {
  visibility: hidden;
}

/* Overlays (@only, @uncover, @alt) off at the step shown (see lpdoc.js,
   which sets lpdoc-ov-off): an @only takes no room then, an @uncover keeps
   it, and an @alt shows its other alternative. */
.lpdoc-only.lpdoc-ov-off,
.lpdoc-alt > .lpdoc-ov-off {
  display: none;
}
.lpdoc-uncover.lpdoc-ov-off {
  visibility: hidden;
}


/* The number of the slide on screen, in the bottom corner: it matches the
   page number of the same deck in print (the cover is 1). Only in slide
   mode, and not on paper, sinde there pages are already numbered. */
.lpdoc-slideno { display: none; }
.lpdoc-slide-mode .lpdoc-slideno {
    display: block;
    position: fixed;
    right: 14px;
    bottom: 10px;
    font-size: 13px;
    color: var(--fgdim);
    user-select: none;
    pointer-events: none;
}
@media print {
    .lpdoc-slide-mode .lpdoc-slideno { display: none; }
}
/* TeX source of a formula, shown when no MathJax is available (see
   using_mathjax/1 in autodoc_html_assets.pl). Marked so that it does not
   read as ordinary code: this is something meant to be typeset that
   could not be. */
.lpdoc-math-src {
  border-bottom: 1px dotted var(--fgdim);
}

/* --------------------------------------------------------------------------- */
/* Style for print */

/* TODO: add some margin/padding while still hiding headers and footers */
@media print {
  @page {
    size: auto;
    /* TODO: CropBox vs MediaBox issues makes the generated PDF do not
       cover the whole screen in macOS preview. Any fix? */
    /* margin: 0; */ /* hide headers and footers */
  }
  @page landscape-page {
    /* size: landscape; */
    size: 297mm 185.625mm; /* A4 width with 16:10 ratio for slides */
    /* margin: 0; */ /* hide headers and footers */
  }
  /* hide headers and footers added by the browser */
  header, footer {
    display: none;
  }

  body {
    margin: 0;
    padding: 0;
    /* make sure that color is not changed, the main use is print to PDF */
    -webkit-print-color-adjust: exact; /* Chrome, Safari, Edge */
    print-color-adjust: exact; /* Modern standard */
  }

  .lpdoc-slide-mode .lpdoc-slide-hide {
    display: block;
  }

  .lpdoc-slide-mode .lpdoc-slide {
    page-break-before: always; /* page break before the element */
  }
  .lpdoc-slide-mode .lpdoc-main {
    page: landscape-page;
  }
  .lpdoc-slide-mode div.lpdoc-clearer {
    display: none;
  }

  /* Reset sidebar position */
  .leftbar > div.lpdoc-main,
  .fixleftbar > div.lpdoc-main { margin-left: 0; }
  .rightbar > div.lpdoc-main,
  .fixrightbar > div.lpdoc-main { margin-right: 0; }
  
  a#sidebar-toggle-button,
  div#sidebar,
  div#sidebar.sidebar-toggled,
  .lpdoc-sidebar,
  .lpdoc-footer {
    display: none;
  }
}