/* Standard Herbie header */

body { width: 800px; margin: 0 auto; font-family: sans; line-height: 1.25; }

a { color: #2A6496; text-decoration: none; cursor: pointer }
a:hover {text-decoration: underline; color: #295785}
figure { margin: 0; }

#large { margin: 2em 0; text-align: center; }
#large div { margin: 0 1em; display: inline-block; vertical-align: top; }
#large .number { font-size: 2em; display: block; }
@media print { #large { margin-top: 0; }}

/* Plots at the top */

figure { display: flex; flex-direction: row; gap: 1em; margin: 2em 0; }
figure div { flex: 1; border: 1px solid #ddd; padding: 1ex; }
figure h2 { font-size: 1em; font-family: 'IBM Plex Serif', serif; margin: 0; }
figure .domain, figure .tick { color: #888; }
figure text { font-family: 'IBM Plex Serif', serif; }
figcaption { font-size: 80%; color: #666; padding-top: 1ex; }
svg.clickable circle:hover { stroke: #00a; stroke-width: 10; cursor: pointer; }

/* Flag list / configuration */

#about { margin: 3em 0; }
#about th { font-weight: bold; text-align: left; padding-right: 1em; }

#flag-list { position: relative; }
#flag-list kbd:not(:last-child):after { content: ", "; }
#flag-list a { float: right; margin: 0 .5em; }
#flag-list a:before { content: "("; }
#flag-list a:after { content: ")"; }
#flag-list #changed-flags { display: none; }
#flag-list #all-flags { display: block; }
#flag-list.changed-flags #changed-flags { display: block; }
#flag-list.changed-flags #all-flags { display: none; }

/* Table of results */

#results { border-collapse: collapse; width:100%; }
#results th { white-space: pre; }
#results td { text-align: right; padding: .5em; overflow: hidden; font-size: 15pt; }
#results tbody tr:hover {background-color: #e0f8d8; cursor: pointer;}

#results a {
    position: absolute; left: 0; right: 0; z-index: 100;
    padding: .5em; margin-top: -1.25em;
}

#results td:nth-child(1) { text-align: left; word-break: break-all; }
#results td:nth-child(6) {width: 0;}

tr.imp-start  td:nth-child(3) {background-color:#87fc70;}
tr.apx-start  td:nth-child(3) {background-color:#ff9500;}
tr.uni-start  td:nth-child(3) {background-color:#ff5e3a;color:#f7f7f7;}
tr.ex-start   td:nth-child(3) {background-color:#e0f8d8;}

tr.gt-target  td:nth-child(3) {background-color:#87fc70;}
tr.gt-target  td:nth-child(4) {background-color:#0bd318;}
tr.eq-target  td:nth-child(3) {background-color:#87fc70;}
tr.eq-target  td:nth-child(4) {background-color:#87fc70;}
tr.lt-target  td:nth-child(3) {background-color:#87fc70;}
tr.lt-target  td:nth-child(4) {background-color:#ff9500;}
tr.eq-start   td:nth-child(3) {background-color:#ff9500;}
tr.eq-start   td:nth-child(4) {background-color:#ffdb4c;}
tr.lt-start   td:nth-child(3) {background-color:#ff5e3a;color: #f7f7f7;}
tr.lt-start   td:nth-child(4) {background-color:#ffdb4c;color: #f7f7f7;}

tr.crash      td:nth-child(3) {background-color:#ff9d87; color:#ed2b00; border: 2px solid #ff5e3a; margin: -2px; }
tr.error      td:nth-child(3) {background-color:#4a4a4a;color:#f7f7f7;}
tr.timeout    td:nth-child(3) {background-color:#8e8e93;color:#f7f7f7;}

#results.no-target td:nth-child(4) {display: none;}
#results.no-target th:nth-child(4) {display: none;}

/* Help button */

.help-button {
 display: inline-block; background: #888;
 font-size: .8em; color: #eee; line-height: 1.3em;
 height: 1.25em; width: 1.25em; border-radius: .625em;
 vertical-align: top; text-align: center;
}
.help-button:hover { background: #444; cursor: pointer; }
h1 > .help-button {
    vertical-align: text-top;
    font-size: small;
    margin-left: 5px;
    background: #ddd;
    color: #999;
    rotate: 270deg;
}

/* Links at the top */
#links { border-bottom: 1px solid #ddd; line-height: 2; overflow: auto; }
#links .right { float: right; }
#links a + a { margin-left: 1em; }

/* Subreports */

#subreports-toggle {
    color: #2A6496;
    text-decoration: none;
    cursor: pointer;
    margin-left: 1em;
}

.active, #subreports-toggle:hover {
    text-decoration: underline;
    color: #295785
}

#subreports.no-subreports #with-subreports { display: none; }
#subreports #with-subreports { display: block; border-top: 1px solid #ddd; }

#subreport-table {
    padding: 5px 0 5px 1em;
}

#subreport-table table {
    border-collapse: collapse;
    border-spacing: 0;
}

#subreport-table table tr th { line-height: 25px; padding-right: 10px; }
#subreport-table table tr td { line-height: 25px; padding-right: 10px; }

/* Detail page layout */

section { margin: 5em 0; position: relative; }
@media print { section { margin: 3em 0; } }
section h1 {
    position: absolute; width: 300px; text-align: left; right: -340px; top: -15px;
    transform: rotate(90deg); transform-origin: top left;
    font-size: 24px; font-weight: normal; color: #aaa;
}

/* Warnings */

.warnings { list-style: inside none; padding: 0; }
.warnings > li {
    margin: .25em 0; padding: .5em; background: #ffdb4c; border: 2px solid #ff9500;
}
.warnings h2 { font-size: 100%; font-weight: normal; margin: 0; }
.warnings h2:before { content: "Warning: "; font-weight: bold; }
.warnings h2 a { float: right; }
.warnings ol { list-style: inside none; padding: 0 1em; }
.warnings ol li { margin: .25em 0; }

/* Big block for program input output */

#program {
    background: #ddd; text-align: center; font-size: 24px;
    position: relative; padding: 1em;
}
@media print { #program { padding: 0; background: transparent; margin: 2em 0; } }
#program .program { display: inline-block; text-align: left; }
#program .arrow { color: transparent; font-size: 0; }
#program .arrow:after { content: "↓"; color: black; font-size: 24px; }
#program.horizontal .arrow { display: inline-block; }
#program.horizontal .arrow:after { margin: 0 1em; content: "→"; font-size: 40px; }
#language { position: absolute; right: 1em; }
#precondition { padding: 0 1em 1em; margin: 0 -1em 1em; border-bottom: 2px solid white; }
#precondition:before { content: "Precondition"; float: left; color: #444; }
/* Allow line breaks in display equations (see https://katex.org/docs/issues.html) */
.katex-display > .katex { white-space: normal }
.katex-display .base { margin: 0.25em 0 }
.katex-display { margin: 0.5em 0; }
#preprocess { padding: 0 1em 1em; margin: 0 -1em 1em; border-bottom: 2px solid white; }
#preprocess:before { content: "Preprocess"; float: left; color: #444; }

/* Error graphs */

#graphs figure { margin: 0 auto; position: relative; padding-top: 300px; width: 800px; }
#graphs figcaption { text-align: left; }
#graphs figure img { position: absolute; top: 0; left: 0; }
#graphs figcaption button {
    float: right; margin: 0 .25em; cursor: pointer;
    border: 3px solid black; background: gray; color: transparent;
    height: 1.5em; width: 1.5em; border-radius: .75em;
    overflow: hidden;
}
#graphs figcaption button.Result { border-color: blue; background: lightblue; }
#graphs figcaption button.Target { border-color: green; background: lightgreen; }
#graphs figcaption button.Input { border-color: red; background: pink; }
#graphs figcaption button.inactive { background: white; }

.tabbar { margin: 0; padding: 0; list-style-type: none; list-style-position: inside; text-align: left; }
.tabbar p { display: inline-block; margin: 0 .5em 0 0}
.tabbar li { padding: .5ex; display: inline-block; margin: .1em; cursor: pointer; }
.tabbar li:hover { background: #e4e4e4; }
.tabbar li.selected { background: #d3d3d3; }

#plot_options { display: grid; grid-template-columns: auto auto; }
#variables { justify-self: start; }
#functions { justify-self: end; }

#variables .selected { background-color: lightgray; }
#variables .variable { margin-right: 3px; padding-left: 2px; padding-right: 2px; padding-bottom: 2px; }

#functions { margin-right: 40px; }
#functions .function {
    width: 20px;
    height: 20px;
    /* border: 1px solid #000; */
    border-radius: 50%;
    /* box-shadow: inset 0px 0px 0px 1px black; */
    box-sizing: border-box; /* Include padding and border in element's width and height */
    display: inline-block;
    margin-left: 5px;
    margin-top: 3px;
    vertical-align: text-bottom;
}

#functions #function_start { border: 3px solid red; }
#functions #function_start.selected { background: pink; }
#functions #function_end { border: 3px solid blue; }
#functions #function_end.selected { background: lightblue; }
#functions #function_target { border: 3px solid green; }
#functions #function_target.selected { background: lightgreen; }

/* Try it out section */

#try-result output { font-size: 108%; margin: 0 .5em; float: right; }
#try-result div { overflow: auto; }
#try-result table { line-height: 1.5; margin-top: .25em; }
#try-result { width: 39%; float: right; }
#try-result p.header { margin: 0 0 .5em; font-size: 120%; color: #444; border-bottom: 1px solid #ccc; line-height: 1.5; }
#try-result label:after { content: ":"; }

#try-inputs-wrapper { width: 59%; display: inline-block; }

#try-inputs ol { list-style: none; padding: 0; display: inline-block; margin: 0 0 0 -1em; }
#try-inputs ol label { min-width: 4ex; text-align: right; margin-right: .5em; display: inline-block; }
#try-inputs li { margin-left: 1em; display: inline-block; font-size: 110%; font-family: monospace; line-height: 2; }
#try-inputs label:after { content: ":"; }
#try-inputs input { padding: 1px 4px; width: 25ex; }
#try-inputs p.header { margin: 0 0 .5em; font-size: 120%; color: #444; border-bottom: 1px solid #ccc; line-height: 1.5; }

#try-error { color:  red; font-size: 120%; display: none; }
.error #try-error { display: block; }
#try-result.error table { display: none; }

/* Derivation */

.history, .history ol { list-style: none inside; width: 800px; margin: 0 0 2em; padding: 0; }

.history li p { width: 150px; display: inline-block; margin: 0 25px 0 0; }
.history li .error { display: block; color: #666; }
.history li > div { display: inline-block; margin: 0; width: 600px; vertical-align: middle; }
.history li > div > div { margin: 0; display: inline-block; text-align: right !important; }

.history h2 { margin: 1.333em 0 .333em; }
.history li { margin: .5em 0; border-top: 1px solid #ddd; padding-top: .5em; }
.history li:first-child { border-top: none; padding-top: 0; }
.history .rule { text-decoration: underline; }
.history .event { display: block; margin: .5em 0; }

.history .proof { width: 100%; overflow: auto; }
.history .proof table { padding: 0 .5em; }
.history .proof table th { text-align: left; font-weight: normal; }
.history .proof table th .info { display: block; color: #666; }
.history .proof table td { text-align: left; }

/* Process / debug info */

#process-info { background: #ddd; }
#process-info p.header { font-size: 110%; padding: 1em 1em .5em; margin: 0; }
#process-info p.header .attachment { float: right; margin: 0 0 0 1em; }
#process-info > p { margin: 1em .75em 0; }

.timeline {
    height: 2em; border: 1px solid #888; border-width: 1px 0px; margin-bottom: 1em;
    display: flex;
}
.timeline-phase { height: 2em; background: var(--phase-color); display: inline-block; }
@media print {
    .timeline { border: none; }
    .timeline-phase { outline: 1px solid black; }
}

/* Blocks of information */

.timeline-block { border-left: 1ex solid var(--phase-color); padding: 1px 1ex;}
.timeline-block h3 { margin: 0; font-size: 110%; font-weight: normal; }
.timeline-block p { margin: 0; }
.timeline-block h3 .time { float: right; }

.timeline-block dl { font-size: 90%; }
.timeline-block dt { min-width: 6em; float: left; font-size: 100%; }
.timeline-block dd { margin: 0 0 1ex 6em; max-width: 100%; overflow: auto; }
table.times { border-spacing: 15px 5px; }
table th { text-align: left; }
table.times td { text-align: right; min-width: 8ex; vertical-align: baseline; }
table.times td:last-child { text-align: left; }
table.states { min-width: 50%; }
table.states td:last-child, table.states tfoot { font-weight: bold; }
table pre { padding: 0; margin: 0; text-align: left; font-size: 110%; }

/* Timeline colors -- Uses Tango color scheme */

.timeline-sample   { --phase-color: #edd400; }
.timeline-analyze  { --phase-color: #fce94f; }

.timeline-eval     { --phase-color: #204a87; }
.timeline-prune    { --phase-color: #3465a4; }
.timeline-localize { --phase-color: #729fcf; }

.timeline-series   { --phase-color: #4e9a06; }
.timeline-rewrite  { --phase-color: #73d216; }
.timeline-simplify { --phase-color: #8ae234; }

.timeline-regimes  { --phase-color: #a40000; }
.timeline-bsearch  { --phase-color: #cc0000; }

/* Bogosity colors */

.bogosity {
    display: flex; margin-bottom: 1em; height: 1em;
    border-radius: .5em; overflow: clip;
}
.bogosity > div { background: var(--phase-color); display: inline-block; }
@media print {
    .bogosity { border: none; }
    .bogosity > div { outline: 1px solid black; }
}

.bogosity-valid { --phase-color: #4e9a06; }
.bogosity-infinite { --phase-color: #8ae234; }
.bogosity-unknown { --phase-color: #000000; }
.bogosity-unsamplable { --phase-color: #a40000; }
.bogosity-invalid { --phase-color: #204a87; }
.bogosity-precondition { --phase-color: #729fcf; }

/* Code sample to reproduce */

#reproduce pre { padding: 1em; margin: 0; font-family: monospace; overflow-x: auto; }
pre.shell code:before { content: "$ "; font-weight: bold; }

/* Target / expected code block */

#comparison table { width: 300px; display: inline-table; vertical-align: top; }
#comparison table th { text-align: left; }
#comparison table td { text-align: right; }
#comparison div { display: inline-block; width: 500px; }

/* Alternatives */

#alternatives table { width: 275px; display: inline-table; vertical-align: top; }
#alternatives table th { text-align: left; font-weight: normal; }
#alternatives table td { text-align: left; width: 75px; }
#alternatives .entry { padding: 5px 0px; }
#alternatives .entry .math { display: inline-block; width: 500px; }

/* Formatting backtraces */

#backtrace table { width: 100%; }
#backtrace th[colspan] { text-align: left; }
#backtrace th { text-align: right; }
#backtrace td:nth-child(3), #backtrace td:nth-child(4) { text-align: right; }
#backtrace td.procedure { font-family: monospace; }

/* Formatting profile info */

.loaded .load-text { display: none; }
.load-text { text-align: center; font-size: 140%; color: #888; }

a.delete { color: currentColor; }
a.delete:hover { color: #ed2b00; text-decoration: line-through; }
#profile { border: 1px solid #ddd; }
#profile input {
    width: 100%; padding: .5ex 1ex; box-sizing: border-box;
    border: none; border-bottom: 1px solid #ddd; font-size: 150%;
}
#profile .profile-row { margin: 1em 0; }
.profile-row div { display: flex; }
#profile .edge { color: #888; margin-left: 2em; }
#profile .node { font-size: 120%; }
#profile .path, #profile .name { font-family: monospace; white-space: nowrap; }
#profile .path { flex-grow: 1; overflow: hidden; text-overflow: ellipsis; }
#profile .path:before { content: " ("; }
#profile .path:after { content: ") "; }
.profile-row > div > * { padding: 0 .5em; }
#profile .pct { width: 4em; text-align: right; }