@charset "UTF-8";
/*
Copyright © 2019 Clément Pit-Claudel

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
*/

.alectryon-coqdoc .doc .code,
.alectryon-coqdoc .doc .comment,
.alectryon-coqdoc .doc .inlinecode,
.alectryon-io, .alectryon-toggle-label, .alectryon-header {
    font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Fira Code', monospace;
    font-feature-settings: "XV00" 1; /* Use Coq ligatures when Iosevka is available */
    line-height: initial;
}

.alectryon-io, .alectryon-toggle-label, .alectryon-header {
    overflow: visible;
    overflow-wrap: break-word;
    position: relative;
    white-space: pre-wrap;
}

/*
CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
respects the user's `bidi-display-reordering` setting), so don't turn it off
here either.  But beware unexpected results like `Definition test_אב := 0.`

.alectryon-io span {
    direction: ltr;
    unicode-bidi: bidi-override;
}

In any case, make an exception for comments:

.highlight .c {
    direction: embed;
    unicode-bidi: initial;
}
*/

.alectryon-toggle,
.alectryon-io .coq-toggle,
.alectryon-io .coq-extra-goals-toggle {
    display: none;
}

.alectryon-bubble,
.alectryon-toggle-label,
.alectryon-io label.coq-input,
.alectryon-io .coq-extra-goals-label {
    cursor: pointer;
}

.alectryon-toggle-label,
.coq-extra-goals-label {
    display: block;
    font-size: 0.8rem;
}

.alectryon-io .coq-input {
    padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
    padding-right: 1rem; /* Prevent line wraps before the checkbox bubble */
}

.alectryon-io .coq-sentence.alectryon-target .coq-input {
    /* FIXME use a background? FIXME if keywords were ‘bolder’ we wouldn't need !important */
    font-weight: bold !important; /* Use !important to avoid a * selector */
}

.alectryon-io .coq-extra-goals-label {
    text-align: right;
}

.alectryon-bubble:before,
.alectryon-toggle-label:before,
.alectryon-io label.coq-input:after,
.alectryon-io .coq-extra-goals-label:before {
    border: 1px solid #babdb6;
    border-radius: 1rem;
    box-sizing: border-box;
    content: '';
    display: inline-block;
    font-weight: bold;
    height: 0.25rem;
    margin-bottom: 0.15rem;
    vertical-align: middle;
    width: 0.75rem;
}

.alectryon-toggle-label:before,
.alectryon-io .coq-extra-goals-label:before {
    margin-right: 0.25rem;
}

.alectryon-io label.coq-input:after {
    margin-left: 0.25rem;
    margin-right: -1rem; /* Compensate for the anti-wrapping space */
}

@media (any-hover: hover) {
    .alectryon-bubble:hover:before,
    .alectryon-toggle-label:hover:before,
    .alectryon-io label.coq-input:hover:after {
        background: #eeeeec;
    }

    .alectryon-io label.coq-input:hover {
        text-decoration: underline dotted #babdb6;
	    text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
    }
}

.alectryon-io .coq-sentence:hover .coq-output {
    z-index: 2; /* Place hovered goals above .coq-sentence.alectryon-target ones */
}

.alectryon-toggle:checked + .alectryon-toggle-label:before,
.alectryon-io .coq-toggle:checked + label.coq-input:after,
.alectryon-io .coq-extra-goals-toggle:checked + .coq-extra-goals-label:before {
    background-color: #babdb6;
    border-color: #babdb6;
}

/* Disable clicks on sentences when the document-wide toggle is set. */
.alectryon-toggle:checked + label + .alectryon-container label.coq-input {
    cursor: unset;
    pointer-events: none;
}

/* Hide individual checkboxes when the document-wide toggle is set. */
.alectryon-toggle:checked + label + .alectryon-container label.coq-input:after {
    display: none;
}

/* .coq-output is displayed by toggles, :hover, and .alectryon-target rules */
.alectryon-io .coq-output {
    box-sizing: border-box;
    display: none;
    left: 0;
    right: 0;
    position: absolute;
    padding: 0.25rem 0;
    z-index: 1; /* Default to an index lower than that used by :hover */
}

.alectryon-io .coq-sentence:hover .coq-output:not(:hover),
.alectryon-io .coq-sentence.alectryon-target .coq-output {
    display: block;
}

.alectryon-io .coq-extra-goals .goal-hyps {
    display: none;
}

.alectryon-io .coq-extra-goals .goal-separator {
    margin-top: 0;
}

/* Show just a small preview of the other goals; this is undone by the
   "extra-goals" toggle and by :hover and .alectryon-target in windowed mode. */
.alectryon-io .coq-extra-goals .goal-conclusion {
    max-height: 5.2em;
    overflow-y: auto;
    /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
       to be added below the box. ‘vertical-align: middle’ gets rid of it. */
    vertical-align: middle;
}

.alectryon-io .coq-goals,
.alectryon-io .coq-responses {
    background: #eeeeec;
    display: block;
    padding: 0.25rem;
}

.coq-response::before {
    content: '📨️';
    float: right;
    text-align: justify;
}

.alectryon-toggle:checked + label + .alectryon-container {
    width: unset;
}

/* Show goals when a toggle is set */
.alectryon-toggle:checked + label + .alectryon-container label.coq-input + .coq-output,
.alectryon-io .coq-sentence .coq-toggle:checked ~ .coq-output {
    display: block;
    position: static;
    width: unset;
    background: unset; /* Override the background set in .alectryon-floating */
    padding: 0.25rem 0; /* Re-assert so that later :hover rules don't override this padding */ 
}

.alectryon-toggle:checked + label + .alectryon-container label.coq-input + .coq-output .goal-hyps,
.alectryon-io .coq-toggle:checked ~ .coq-output .goal-hyps {
    flex-flow: row;
    flex-wrap: wrap;
    justify-content: flex-start;
}

.alectryon-toggle:checked + label + .alectryon-container .coq-output > .coq-output-sticky-wrapper,
.alectryon-io .coq-toggle:checked ~ .coq-output > .coq-output-sticky-wrapper {
    display: block;
    margin-bottom: unset; /* Undo negative margins FIXME these margins should be conditional on not checked used to widen the sticky range */
}

.alectryon-io .coq-extra-goals-toggle:checked + label + .coq-extra-goals .goal-hyps {
    display: flex;
}

.alectryon-io .coq-extra-goals-toggle:checked + label + .coq-extra-goals .goal-separator {
    margin-top: 0.5rem; /* Restore hidden margin */
}

.alectryon-io .coq-extra-goals-toggle:checked + label + .coq-extra-goals .goal-conclusion {
    max-height: unset;
    overflow-y: unset;
}

.alectryon-toggle:checked + label + .alectryon-container .coq-toggle ~ .coq-wsp,
.alectryon-io .coq-toggle:checked ~ .coq-wsp {
    display: none;
}

.alectryon-io .coq-responses,
.alectryon-io .coq-response,
.alectryon-io .coq-goals,
.alectryon-io .coq-goal,
.alectryon-io .goal-hyp,
.alectryon-io .goal-conclusion {
    border-radius: 0.15rem;
}

.alectryon-io .coq-goal,
.alectryon-io .coq-response,
.alectryon-io .coq-extra-goals-label {
    margin: 0.25rem;
}

.alectryon-io .coq-goal,
.alectryon-io .coq-response {
    align-items: center;
    background: #d3d7cf;
    display: block;
    flex-direction: column;
    padding: 0.5rem;
    position: relative;
}

.alectryon-io .goal-hyps {
    align-content: space-around;
    align-items: baseline;
    display: flex;
    flex-flow: column; /* row wrap? */
    justify-content: space-around;
    /* FIXME use a ‘gap’ property instead of margins once supported */
    margin: -0.15rem -1rem; /* -0.15rem to cancel the item spacing */
}

.alectryon-io .goal-hyp,
.alectryon-io .goal-conclusion {
    background: #eeeeec;
    display: inline-block;
    padding: 0.15rem 0.35rem;
}

.alectryon-io .goal-hyp {
    display: inline-flex;
    margin: 0.15rem 1rem;
    z-index: 1;
}

.alectryon-io .hyp-names {
    font-weight: 600;
    /* Shrink the list of names, but let it grow as long as space is available. */
    flex-basis: min-content;
    flex-grow: 1;
}

.alectryon-io .hyp-punct {
    font-weight: 600;
    margin: 0 0.5rem;
}

.alectryon-io .hyp-body,
.alectryon-io .hyp-type {
    display: flex;
    vertical-align: top;
}

.alectryon-io .goal-separator {
    align-items: center;
    display: flex;
    flex-direction: row;
}

.alectryon-io .goal-separator hr {
    border: none;
    border-top: thin solid #555753;
    box-sizing: content-box;
    display: block;
    flex-grow: 1;
    height: 0;
    margin: 0.5rem 0;
}

.alectryon-io .goal-separator .goal-name {
    font-size: 0.75em;
    margin-left: 0.5em;
}

/**********/
/* Header */
/**********/

.alectryon-header {
    background: #eeeeec;
    border: 1px solid #babcbd;
    font-size: 0.75em;
    padding: 0.25rem;
    text-align: center;
    margin: 1rem 0;
}

.alectryon-header a {
    cursor: pointer;
    text-decoration: underline;
}

.alectryon-header kbd {
    background: #d3d7cf;
    border-radius: 0.15em;
    border: 1px solid #babdb6;
    box-sizing: border-box;
    display: inline-block;
    font-family: inherit;
    font-size: 0.9em;
    height: 1.3em;
    line-height: 1.2em;
    margin: -0.25em 0;
    padding: 0 0.25em;
    vertical-align: middle;
}

/******************/
/* Floating style */
/******************/

/* FIXME: condition on not checked should also condition on not global-toggled? */

/* If there's space, display goals to the right of the code, not below it. */
@media (min-width: 90rem) {
    .alectryon-floating .alectryon-io {
        /* FIXME: needed? */
        box-sizing: border-box; /* Needed so .coq-output won't overflow */
    }

    /* Adjoin to increase specificity */
    .alectryon-floating .coq-sentence.alectryon-target .coq-output,
    .alectryon-floating .coq-sentence:hover .coq-output {
        bottom: 0;
        left: 100%;
        right: -100%;
        padding: 0 0.5rem;
    }

    .alectryon-floating .coq-output {
        min-height: 100%;
    }

    .alectryon-floating .coq-sentence:hover .coq-output {
        background: white; /* Ensure that short goals hide long ones */
    }

    /* This odd margin-bottom property prevents the sticky div from bumping
       against the bottom of its container (.coq-output).  The alternative
       would be enlarging .coq-output, but that would cause overflows,
       enlarging scrollbars and yielding scrolling towards the bottom of the
       page.  Doing things this way instead makes it possible to restrict
       .coq-output to a reasonable size (100%, through top = bottom = 0).
       See also https://stackoverflow.com/questions/43909940/. */
    .alectryon-floating .coq-output-sticky-wrapper {
        margin-bottom: -200%;
        position: sticky;
        top: 0;
    }

    /* Float underneath the current fragment
    @media (max-width: 90rem) {
        .alectryon-floating .coq-output {
            top: 100%;
        }
    } */
}

/********************/
/* Multi-pane style */
/********************/

.alectryon-windowed {
    border: 0 solid #2e3436;
    box-sizing: border-box;
}

.alectryon-windowed .coq-sentence:hover .coq-output {
    background: white; /* Ensure that short goals hide long ones */
}

.alectryon-windowed .coq-output {
    position: fixed; /* Overwritten by the ‘:checked’ rules */
}

.alectryon-windowed .coq-sentence:hover .coq-output,
.alectryon-windowed .coq-sentence.alectryon-target .coq-output {
    padding: 0.5rem;
    overflow-y: auto; /* Windowed contents may need to scroll */
}

.alectryon-windowed .coq-sentence.alectryon-target .coq-extra-goals .goal-conclusion
/* Like .alectryon-io .coq-extra-goals-toggle:checked + label + .coq-extra-goals .goal-conclusion */ {
    max-height: unset;
    overflow-y: unset;
}

.alectryon-windowed .coq-output-sticky-wrapper {
    display: flex; /* Put messages after goals */
    flex-direction: column-reverse;
}

/*********************/
/* Standalone styles */
/*********************/

.alectryon-standalone {
    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
}

/* Coqdoc */

.alectryon-coqdoc .doc .code,
.alectryon-coqdoc .doc .inlinecode,
.alectryon-coqdoc .doc .comment {
    display: inline;
}

.alectryon-coqdoc .doc .comment {
    color: #eeeeec;
}

.alectryon-coqdoc .doc .paragraph {
    height: 0.75rem;
}

/* Centered */

.alectryon-standalone.alectryon-centered {
    max-width: 50rem;
    margin: auto;
}

/* Floating */

.alectryon-standalone.alectryon-floating {
    max-width: 80rem;
    margin: auto;
}

.alectryon-standalone.alectryon-floating > * {
    width: 50%;
    margin-left: 0;
}

/* Windowed */

.alectryon-standalone.alectryon-windowed {
    display: block;
    margin: 0;
    overflow-y: auto;
    position: absolute;
    padding: 0 1rem;
}

.alectryon-standalone.alectryon-windowed > * {
    margin-left: 0;
}

.alectryon-standalone.alectryon-windowed .alectryon-io {
    box-sizing: border-box;
    width: 100%;
}

/* No need to predicate the rules below on ‘:not(:checked)’, since ‘left’,
   ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
   ‘position’ to ‘static’ */

@media screen and (min-width: 60rem) {
    .alectryon-standalone.alectryon-windowed {
        border-right-width: thin;
        bottom: 0;
        left: 0;
        right: 50%;
        top: 0;
    }

    .alectryon-standalone.alectryon-windowed .coq-sentence:hover .coq-output,
    .alectryon-standalone.alectryon-windowed .coq-sentence.alectryon-target .coq-output {
        bottom: 0;
        left: 50%;
        right: 0;
        top: 0;
    }
}

@media screen and (max-width: 60rem) {
    .alectryon-standalone.alectryon-windowed {
        border-bottom-width: 1px;
        bottom: 40%;
        left: 0;
        right: 0;
        top: 0;
    }

    .alectryon-standalone.alectryon-windowed .coq-sentence:hover .coq-output,
    .alectryon-standalone.alectryon-windowed .coq-sentence.alectryon-target .coq-output {
        bottom: 0;
        left: 0;
        right: 0;
        top: 60%;
    }
}
