diff options
Diffstat (limited to 'docs/proof/alectryon.css')
| -rw-r--r-- | docs/proof/alectryon.css | 657 |
1 files changed, 657 insertions, 0 deletions
diff --git a/docs/proof/alectryon.css b/docs/proof/alectryon.css new file mode 100644 index 0000000..0454c64 --- /dev/null +++ b/docs/proof/alectryon.css @@ -0,0 +1,657 @@ +@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. +*/ + +/*******************************/ +/* CSS reset for .alectryon-io */ +/*******************************/ + +.alectryon-io .highlight { + background: none; /* Some Sphinx themes set a background on .highlight */ +} + +.alectryon.io blockquote { + line-height: inherit; +} + +.alectryon-io label { + display: inline; + font-size: inherit; + margin: 0; +} + +/* Undo <small> and <blockquote>, added to improve RSS rendering. */ + +.alectryon-io small.coq-output { + font-size: inherit; +} + +.alectryon-io blockquote.coq-goal, +.alectryon-io blockquote.coq-message { + font-weight: normal; + font-size: inherit; +} + +/***************/ +/* Main styles */ +/***************/ + +.alectryon-coqdoc .doc .code, +.alectryon-coqdoc .doc .comment, +.alectryon-coqdoc .doc .inlinecode, +pre.alectryon-io, .alectryon-toggle-label, .alectryon-header { + font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', '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-goal-toggle { + display: none; +} + +.alectryon-bubble, +.alectryon-toggle-label, +.alectryon-io label.coq-input, +.alectryon-io .coq-extra-goal-label { + cursor: pointer; +} + +.alectryon-toggle-label, +.coq-extra-goal-label { + display: block; + font-size: 0.8rem; +} + +.alectryon-io .coq-input { + padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */ +} + +.alectryon-io .coq-sentence.alectryon-target .coq-input { + /* FIXME if keywords were ‘bolder’ we wouldn't need !important */ + font-weight: bold !important; /* Use !important to avoid a * selector */ +} + +.alectryon-bubble:before, +.alectryon-toggle-label:before, +.alectryon-io label.coq-input:after, +.alectryon-io .coq-extra-goal-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-goal-label:before { + margin-right: 0.25rem; +} + +.alectryon-io .coq-extra-goal-label::before { + margin-top: -0.35rem; +} + +.alectryon-io label.coq-input { + padding-right: 1rem; /* Prevent line wraps before the checkbox bubble */ +} + +.alectryon-io label.coq-input:after { + margin-left: 0.25rem; + margin-right: -1rem; /* Compensate for the anti-wrapping space */ +} + +.alectryon-failed { + /* Underlines are broken in Chrome (they reset at each element boundary)… */ + /* text-decoration: red wavy underline; */ + /* … but it isn't too noticeable with dots */ + text-decoration: red dotted underline; + text-decoration-skip-ink: none; + /* Chrome prints background images in low resolution, yielding a blurry underline */ + /* background: bottom / 0.3rem auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */ +} + +/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence + doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to + hide its output causes it to remain visible (its :hover state gets triggered. + We only do it for the default style though, since other styles don't put the + output over the main text, so showing too much is not an issue. */ +@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-goal-toggle:checked + .coq-goal .coq-extra-goal-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; + overflow: visible; /* Let box-shadows overflow */ + z-index: 1; /* Default to an index lower than that used by :hover */ +} + +@media (any-hover: hover) { /* See note above about this @media query */ + .alectryon-io .coq-sentence:hover .coq-output:not(:hover) { + display: block; + } +} + +.alectryon-io .coq-sentence.alectryon-target .coq-output { + display: block; +} + +/* Indicate active (hovered or targeted) goals with a shadow. */ +.alectryon-io .coq-sentence:hover .coq-output:not(:hover) .coq-messages, +.alectryon-io .coq-sentence.alectryon-target .coq-output .coq-messages, +.alectryon-io .coq-sentence:hover .coq-output:not(:hover) .coq-goals, +.alectryon-io .coq-sentence.alectryon-target .coq-output .coq-goals { + box-shadow: 0 0 3px gray; +} + +.alectryon-io .coq-extra-goals .coq-goal .goal-hyps { + display: none; +} + +.alectryon-io .coq-extra-goals .coq-extra-goal-toggle:not(:checked) + .coq-goal label.goal-separator hr { + /* Dashes indicate that the hypotheses are hidden */ + border-top-style: dashed; +} + + +/* Show just a small preview of the other goals; this is undone by the + "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */ +.alectryon-io .coq-extra-goals .coq-goal .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-messages { + background: #eeeeec; + border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */ + display: block; + padding: 0.25rem; +} + +.coq-message::before { + content: ''; + float: right; + /* etc/svg/square-bubble-xl.svg */ + background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat; + height: 14px; + width: 14px; +} + +.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 backgrounds set in floating in windowed mode */ + 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 { + /* Overridden back in windowed style */ + flex-flow: row wrap; + justify-content: flex-start; +} + +.alectryon-toggle:checked + label + .alectryon-container .coq-sentence .coq-output > .coq-output-sticky-wrapper, +.alectryon-io .coq-sentence .coq-toggle:checked ~ .coq-output > .coq-output-sticky-wrapper { + display: block; +} + +.alectryon-io .coq-extra-goal-toggle:checked + .coq-goal .goal-hyps { + display: flex; +} + +.alectryon-io .coq-extra-goal-toggle:checked + .coq-goal .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-messages, +.alectryon-io .coq-message, +.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-message { + margin: 0.25rem; +} + +.alectryon-io .coq-goal, +.alectryon-io .coq-message { + 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 nowrap; /* re-stated in windowed mode */ + justify-content: space-around; + /* LATER use a ‘gap’ property instead of margins once supported */ + margin: -0.15rem -0.25rem; /* -0.15rem to cancel the item spacing */ + padding-bottom: 0.5rem; +} + +.alectryon-io .goal-hyp, +.alectryon-io .goal-conclusion { + background: #eeeeec; + display: inline-block; + padding: 0.15rem 0.35rem; +} + +.alectryon-io .goal-hyp { + align-items: baseline; + display: inline-flex; + margin: 0.15rem 0.25rem; + 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-block, +.alectryon-io .hyp-type-block { + display: flex; + align-items: baseline; +} + +.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 0 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 */ +/******************/ + +/* If there's space, display goals to the right of the code, not below it. */ +@media (min-width: 80rem) { + /* Unlike the windowed case, we don't want to move output blocks to the side + when they are both :checked and -targeted, since it gets confusing as + things jump around; hence the commented-output part of the selector, + which would otherwise increase specificity */ + .alectryon-floating .coq-sentence.alectryon-target /* .coq-toggle ~ */ .coq-output, + .alectryon-floating .coq-sentence:hover .coq-output { + top: 0; + left: 100%; + right: -100%; + padding: 0 0.5rem; + position: absolute; + } + + .alectryon-floating .coq-output { + min-height: 100%; + } + + .alectryon-floating .coq-sentence:hover .coq-output { + background: #fdf6e3; /* 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/. */ + /* See note on specificity above */ + .alectryon-floating .coq-sentence.alectryon-target /* .coq-toggle ~ */ .coq-output .coq-output-sticky-wrapper, + .alectryon-floating .coq-sentence:hover .coq-output-sticky-wrapper { + margin-bottom: -200%; + position: sticky; + top: 0; + } + + .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .coq-sentence .coq-output > .coq-output-sticky-wrapper, + .alectryon-floating .alectryon-io .coq-sentence .coq-toggle:checked ~ .coq-output > .coq-output-sticky-wrapper { + margin-bottom: unset; /* Undo the margin */ + } + + /* Float underneath the current fragment + @media (max-width: 80rem) { + .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: #fdf6e3; /* Ensure that short goals hide long ones */ +} + +.alectryon-windowed .coq-output { + position: fixed; /* Overwritten by the ‘:checked’ rules */ +} + +/* See note about specificity below */ +.alectryon-windowed .coq-sentence:hover .coq-output, +.alectryon-windowed .coq-sentence.alectryon-target .coq-toggle ~ .coq-output { + padding: 0.5rem; + overflow-y: auto; /* Windowed contents may need to scroll */ +} + +.alectryon-windowed .alectryon-io .coq-sentence:hover .coq-output:not(:hover) .coq-messages, +.alectryon-windowed .alectryon-io .coq-sentence.alectryon-target .coq-output .coq-messages, +.alectryon-windowed .alectryon-io .coq-sentence:hover .coq-output:not(:hover) .coq-goals, +.alectryon-windowed .alectryon-io .coq-sentence.alectryon-target .coq-output .coq-goals { + box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */ +} + +.alectryon-windowed .alectryon-io .coq-sentence.alectryon-target .coq-output .goal-hyps { + /* Restated to override the :checked style */ + flex-flow: column nowrap; + justify-content: space-around; +} + + +.alectryon-windowed .coq-sentence.alectryon-target .coq-extra-goals .coq-goal .goal-conclusion +/* Like .alectryon-io .coq-extra-goal-toggle:checked + .coq-goal .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; +} + +@media screen and (min-width: 50rem) { + html.alectryon-standalone { + /* Prevent flickering when hovering a block causes scrollbars to appear. */ + margin-left: calc(100vw - 100%); + margin-right: 0; + } +} + +/* 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, Floating */ + +.alectryon-standalone .alectryon-centered, +.alectryon-standalone .alectryon-floating { + max-width: 50rem; + margin: auto; +} + +@media (min-width: 80rem) { + .alectryon-standalone .alectryon-floating { + max-width: 80rem; + } + + .alectryon-standalone .alectryon-floating > * { + width: 40rem; + margin-left: 0; + } +} + +/* Windowed */ + +.alectryon-standalone .alectryon-windowed { + display: block; + margin: 0; + overflow-y: auto; + position: absolute; + padding: 0 1rem; +} + +.alectryon-standalone .alectryon-windowed > * { + /* Override properties of docutils_basic.css */ + margin-left: 0; + max-width: unset; +} + +.alectryon-standalone .alectryon-windowed .alectryon-io { + box-sizing: border-box; + width: 100%; +} + +/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’, + ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting + ‘position’ to ‘static’ */ + + +/* Specificity: We want the output to stay inline when hovered while unfolded + (:checked), but we want it to move when it's targeted (i.e. when the user + is browsing goals one by one using the keyboard, in which case we want to + goals to appear in consistent locations). The selectors below ensure + that :hover < :checked < -targeted in terms of specificity. */ +/* LATER: Reimplement this stuff with CSS variables */ +.alectryon-windowed .coq-sentence.alectryon-target .coq-toggle ~ .coq-output { + position: fixed; +} + +@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%; + } +} |