123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783 |
- body {
- display: flex;
- font-size: 18px;
- line-height: 1.5;
- font-family: Cambria, Palatino Linotype, Palatino, Liberation Serif, serif;
- padding: 0;
- margin: 0;
- color: #111;
- }
-
- #spec-container {
- padding-left: 20px;
- flex-grow: 1;
- flex-basis: 66%;
- box-sizing: border-box;
- overflow: hidden;
- }
-
- body.oldtoc {
- margin: 0 auto;
- }
-
- a {
- text-decoration: none;
- color: #206ca7;
- }
-
- a:visited {
- color: #206ca7;
- }
-
- a:hover {
- text-decoration: underline;
- color: #239dee;
- }
-
-
- code {
- font-weight: bold;
- font-family: Consolas, Monaco, monospace;
- white-space: pre;
- }
-
- pre code {
- font-weight: inherit;
- }
-
- pre code.hljs {
- background-color: #fff;
- margin: 0;
- padding: 0;
- }
-
- ol.toc {
- list-style: none;
- padding-left: 0;
- }
-
- ol.toc ol.toc {
- padding-left: 2ex;
- list-style: none;
- }
-
- var {
- color: #2aa198;
- transition: background-color 0.25s ease;
- cursor: pointer;
- }
-
- var.referenced {
- background-color: #ffff33;
- }
-
- emu-const {
- font-family: sans-serif;
- }
-
- emu-val {
- font-weight: bold;
- }
- emu-alg ol, emu-alg ol ol ol ol {
- list-style-type: decimal;
- }
-
- emu-alg ol ol, emu-alg ol ol ol ol ol {
- list-style-type: lower-alpha;
- }
-
- emu-alg ol ol ol, ol ol ol ol ol ol {
- list-style-type: lower-roman;
- }
-
- emu-eqn {
- display: block;
- margin-left: 4em;
- }
-
- emu-eqn.inline {
- display: inline;
- margin: 0;
- }
-
- emu-eqn div:first-child {
- margin-left: -2em;
- }
-
- emu-note {
- margin: 1em 0;
- color: #666;
- border-left: 5px solid #ccc;
- display: flex;
- flex-direction: row;
- }
-
- emu-note > span.note {
- flex-basis: 100px;
- min-width: 100px;
- flex-grow: 0;
- flex-shrink: 1;
- text-transform: uppercase;
- padding-left: 5px;
- }
-
- emu-note[type=editor] {
- border-left-color: #faa;
- }
-
- emu-note > div.note-contents {
- flex-grow: 1;
- flex-shrink: 1;
- }
-
- emu-note > div.note-contents > p:first-child {
- margin-top: 0;
- }
-
- emu-note > div.note-contents > p:last-child {
- margin-bottom: 0;
- }
-
- emu-example {
- display: block;
- margin: 1em 3em;
- }
-
- emu-example figure figcaption {
- margin-top: 0.5em;
- text-align: left;
- }
-
- emu-production {
- display: block;
- margin-top: 1em;
- margin-bottom: 1em;
- margin-left: 5ex;
- }
-
-
- emu-grammar.inline, emu-production.inline,
- emu-grammar.inline emu-production emu-rhs, emu-production.inline emu-rhs {
- display: inline;
- }
-
- emu-grammar[collapsed] emu-production, emu-production[collapsed] {
- margin: 0;
- }
-
- emu-grammar[collapsed] emu-production emu-rhs, emu-production[collapsed] emu-rhs {
- display: inline;
- padding-left: 1ex;
- }
-
- emu-constraints {
- font-size: .75em;
- margin-right: 1ex;
- }
-
- emu-gann {
- margin-right: 1ex;
- }
-
- emu-gann emu-t:last-child,
- emu-gann emu-nt:last-child {
- margin-right: 0;
- }
-
- emu-geq {
- margin-left: 1ex;
- font-weight: bold;
- }
-
- emu-oneof {
- font-weight: bold;
- margin-left: 1ex;
- }
-
- emu-nt {
- display: inline-block;
- font-style: italic;
- white-space: nowrap;
- text-indent: 0;
- }
-
- emu-nt a, emu-nt a:visited {
- color: #333;
- }
-
- emu-rhs emu-nt {
- margin-right: 1ex;
- }
-
- emu-t {
- display: inline-block;
- font-family: monospace;
- font-weight: bold;
- white-space: nowrap;
- text-indent: 0;
- }
-
- emu-production emu-t {
- margin-right: 1ex;
- }
-
- emu-rhs {
- display: block;
- padding-left: 75px;
- text-indent: -25px;
- }
-
- emu-mods {
- font-size: .85em;
- vertical-align: sub;
- font-style: normal;
- font-weight: normal;
- }
-
- emu-production[collapsed] emu-mods {
- display: none;
- }
-
- emu-params, emu-opt {
- margin-right: 1ex;
- font-family: monospace;
- }
-
- emu-params, emu-constraints {
- color: #2aa198;
- }
-
- emu-opt {
- color: #b58900;
- }
-
- emu-gprose {
- font-size: 0.9em;
- font-family: Helvetica, Arial, sans-serif;
- }
-
- h1.shortname {
- color: #f60;
- font-size: 1.5em;
- margin: 0;
- }
-
- h1.version {
- color: #f60;
- font-size: 1.5em;
- margin: 0;
- }
-
- h1.title {
- margin-top: 0;
- color: #f60;
- }
-
- h1.first {
- margin-top: 0;
- }
-
- h1, h2, h3, h4, h5, h6 {
- position: relative;
- }
-
- h1 .secnum {
- text-decoration: none;
- margin-right: 10px;
- }
-
- h1 span.title {
- order: 2;
- }
-
-
- h1 { font-size: 2.67em; margin-top: 2em; margin-bottom: 1em; line-height: 1em;}
- h2 { font-size: 2em; }
- h3 { font-size: 1.56em; }
- h4 { font-size: 1.25em; }
- h5 { font-size: 1.11em; }
- h6 { font-size: 1em; }
-
- h1:hover span.utils {
- display: block;
- }
-
- span.utils {
- font-size: 18px;
- line-height: 18px;
- display: none;
- position: absolute;
- top: 100%;
- left: 0;
- right: 0;
- font-weight: normal;
- }
-
- span.utils:before {
- content: "⤷";
- display: inline-block;
- padding: 0 5px;
- }
-
- span.utils > * {
- display: inline-block;
- margin-right: 20px;
- }
-
- h1 span.utils span.anchor a,
- h2 span.utils span.anchor a,
- h3 span.utils span.anchor a,
- h4 span.utils span.anchor a,
- h5 span.utils span.anchor a,
- h6 span.utils span.anchor a {
- text-decoration: none;
- font-variant: small-caps;
- }
-
- h1 span.utils span.anchor a:hover,
- h2 span.utils span.anchor a:hover,
- h3 span.utils span.anchor a:hover,
- h4 span.utils span.anchor a:hover,
- h5 span.utils span.anchor a:hover,
- h6 span.utils span.anchor a:hover {
- color: #333;
- }
-
- emu-intro h1, emu-clause h1, emu-annex h1 { font-size: 2em; }
- emu-intro h2, emu-clause h2, emu-annex h2 { font-size: 1.56em; }
- emu-intro h3, emu-clause h3, emu-annex h3 { font-size: 1.25em; }
- emu-intro h4, emu-clause h4, emu-annex h4 { font-size: 1.11em; }
- emu-intro h5, emu-clause h5, emu-annex h5 { font-size: 1em; }
- emu-intro h6, emu-clause h6, emu-annex h6 { font-size: 0.9em; }
- emu-intro emu-intro h1, emu-clause emu-clause h1, emu-annex emu-annex h1 { font-size: 1.56em; }
- emu-intro emu-intro h2, emu-clause emu-clause h2, emu-annex emu-annex h2 { font-size: 1.25em; }
- emu-intro emu-intro h3, emu-clause emu-clause h3, emu-annex emu-annex h3 { font-size: 1.11em; }
- emu-intro emu-intro h4, emu-clause emu-clause h4, emu-annex emu-annex h4 { font-size: 1em; }
- emu-intro emu-intro h5, emu-clause emu-clause h5, emu-annex emu-annex h5 { font-size: 0.9em; }
- emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex h1 { font-size: 1.25em; }
- emu-intro emu-intro emu-intro h2, emu-clause emu-clause emu-clause h2, emu-annex emu-annex emu-annex h2 { font-size: 1.11em; }
- emu-intro emu-intro emu-intro h3, emu-clause emu-clause emu-clause h3, emu-annex emu-annex emu-annex h3 { font-size: 1em; }
- emu-intro emu-intro emu-intro h4, emu-clause emu-clause emu-clause h4, emu-annex emu-annex emu-annex h4 { font-size: 0.9em; }
- emu-intro emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex emu-annex h1 { font-size: 1.11em; }
- emu-intro emu-intro emu-intro emu-intro h2, emu-clause emu-clause emu-clause emu-clause h2, emu-annex emu-annex emu-annex emu-annex h2 { font-size: 1em; }
- emu-intro emu-intro emu-intro emu-intro h3, emu-clause emu-clause emu-clause emu-clause h3, emu-annex emu-annex emu-annex emu-annex h3 { font-size: 0.9em; }
- emu-intro emu-intro emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex emu-annex emu-annex h1 { font-size: 1em; }
- emu-intro emu-intro emu-intro emu-intro emu-intro h2, emu-clause emu-clause emu-clause emu-clause emu-clause h2, emu-annex emu-annex emu-annex emu-annex emu-annex h2 { font-size: 0.9em; }
- emu-intro emu-intro emu-intro emu-intro emu-intro emu-intro h1, emu-clause emu-clause emu-clause emu-clause emu-clause emu-clause h1, emu-annex emu-annex emu-annex emu-annex emu-annex emu-annex h1 { font-size: 0.9em }
-
- emu-clause {
- display: block;
- }
-
- /* Figures and tables */
- figure { display: block; margin: 1em 0 3em 0; }
- figure object { display: block; margin: 0 auto; }
- figure table.real-table { margin: 0 auto; }
- figure figcaption {
- display: block;
- color: #555555;
- font-weight: bold;
- text-align: center;
- }
-
- emu-table table {
- margin: 0 auto;
- }
-
- emu-table table, table.real-table {
- border-collapse: collapse;
- }
-
- emu-table td, emu-table th, table.real-table td, table.real-table th {
- border: 1px solid black;
- padding: 0.4em;
- vertical-align: baseline;
- }
- emu-table th, emu-table thead td, table.real-table th {
- background-color: #eeeeee;
- }
-
- /* Note: the left content edges of table.lightweight-table >tbody >tr >td
- and div.display line up. */
- table.lightweight-table {
- border-collapse: collapse;
- margin: 0 0 0 1.5em;
- }
- table.lightweight-table td, table.lightweight-table th {
- border: none;
- padding: 0 0.5em;
- vertical-align: baseline;
- }
-
- /* diff styles */
- ins {
- background-color: #e0f8e0;
- text-decoration: none;
- border-bottom: 1px solid #396;
- }
-
- del {
- background-color: #fee;
- }
-
- ins.block, del.block,
- emu-production > ins, emu-production > del,
- emu-grammar > ins, emu-grammar > del {
- display: block;
- }
-
- /* Menu Styles */
- #menu-toggle {
- font-size: 2em;
-
- position: fixed;
- top: 0;
- left: 0;
- width: 1.5em;
- height: 1.5em;
- z-index: 3;
- visibility: hidden;
- color: #1567a2;
- background-color: #fff;
-
- line-height: 1.5em;
- text-align: center;
- -webkit-touch-callout: none;
- -webkit-user-select: none;
- -khtml-user-select: none;
- -moz-user-select: none;
- -ms-user-select: none;
- user-select: none;;
-
- cursor: pointer;
- }
-
- #menu {
- display: flex;
- flex-direction: column;
- width: 33%; height: 100vh;
- max-width: 500px;
- box-sizing: border-box;
- background-color: #ddd;
- overflow: hidden;
- transition: opacity 0.1s linear;
- padding: 0 5px;
- position: fixed;
- left: 0; top: 0;
-
- z-index: 2;
- }
-
- #menu-spacer {
- flex-basis: 33%;
- max-width: 500px;
- flex-grow: 0;
- flex-shrink: 0;
- }
-
- #menu a {
- color: #1567a2;
- }
-
- #menu.active {
- display: flex;
- opacity: 1;
- z-index: 2;
- }
-
- #menu-pins {
- flex-grow: 1;
- display: none;
- }
-
- #menu-pins.active {
- display: block;
- }
-
- #menu-pins-list {
- margin: 0;
- padding: 0;
- counter-reset: pins-counter;
- }
-
- #menu-pins-list > li:before {
- content: counter(pins-counter);
- counter-increment: pins-counter;
- display: inline-block;
- width: 25px;
- text-align: center;
- border: 1px solid #bbb;
- padding: 2px;
- margin: 4px;
- box-sizing: border-box;
- line-height: 1em;
- background-color: #ccc;
- border-radius: 4px;
- }
- #menu-toc > ol {
- padding: 0;
- flex-grow: 1;
- }
-
- #menu-toc > ol li {
- padding: 0;
- }
-
- #menu-toc > ol , #menu-toc > ol ol {
- list-style-type: none;
- margin: 0;
- padding: 0;
- }
-
- #menu-toc > ol ol {
- padding-left: 0.75em;
- }
-
- #menu-toc li {
- text-overflow: ellipsis;
- overflow: hidden;
- white-space: nowrap;
- }
-
- #menu-toc .item-toggle {
- display: inline-block;
- transform: rotate(-45deg) translate(-5px, -5px);
- transition: transform 0.1s ease;
- text-align: center;
- width: 20px;
-
- color: #aab;
-
- -webkit-touch-callout: none;
- -webkit-user-select: none;
- -khtml-user-select: none;
- -moz-user-select: none;
- -ms-user-select: none;
- user-select: none;;
-
- cursor: pointer;
- }
-
- #menu-toc .item-toggle-none {
- display: inline-block;
- width: 20px;
- }
-
- #menu-toc li.active > .item-toggle {
- transform: rotate(45deg) translate(-5px, -5px);
- }
-
- #menu-toc li > ol {
- display: none;
- }
-
- #menu-toc li.active > ol {
- display: block;
- }
-
- #menu-toc li.revealed > a {
- background-color: #bbb;
- font-weight: bold;
- /*
- background-color: #222;
- color: #c6d8e4;
- */
- }
-
- #menu-toc li.revealed-leaf> a {
- color: #206ca7;
- /*
- background-color: #222;
- color: #c6d8e4;
- */
- }
-
- #menu-toc li.revealed > .item-toggle {
- transform: rotate(45deg) translate(-5px, -5px);
- }
-
- #menu-toc li.revealed > ol {
- display: block;
- }
-
- #menu-toc li > a {
- padding: 2px 5px;
- }
-
- #menu > * {
- margin-bottom: 5px;
- }
-
- .menu-pane-header {
- padding: 0 5px;
- text-transform: uppercase;
- background-color: #aaa;
- color: #335;
- font-weight: bold;
- letter-spacing: 2px;
- flex-grow: 0;
- flex-shrink: 0;
- font-size: 0.8em;
- }
-
- #menu-toc {
- display: flex;
- flex-direction: column;
- width: 100%;
- overflow: hidden;
- flex-grow: 1;
- }
-
- #menu-toc ol.toc {
- overflow-x: hidden;
- overflow-y: auto;
- }
-
- #menu-search {
- position: relative;
- flex-grow: 0;
- flex-shrink: 0;
- width: 100%;
-
- display: flex;
- flex-direction: column;
-
- max-height: 300px;
- }
-
- #menu-trace-list {
- display: none;
- }
-
- #menu-search-box {
- box-sizing: border-box;
- display: block;
- width: 100%;
- margin: 5px 0 0 0;
- font-size: 1em;
- padding: 2px;
- background-color: #bbb;
- border: 1px solid #999;
- }
-
- #menu-search-results {
- overflow-x: hidden;
- overflow-y: auto;
- }
-
- li.menu-search-result-clause:before {
- content: 'clause';
- width: 40px;
- display: inline-block;
- text-align: right;
- padding-right: 1ex;
- color: #666;
- font-size: 75%;
- }
- li.menu-search-result-op:before {
- content: 'op';
- width: 40px;
- display: inline-block;
- text-align: right;
- padding-right: 1ex;
- color: #666;
- font-size: 75%;
- }
-
- li.menu-search-result-prod:before {
- content: 'prod';
- width: 40px;
- display: inline-block;
- text-align: right;
- padding-right: 1ex;
- color: #666;
- font-size: 75%
- }
-
-
- li.menu-search-result-term:before {
- content: 'term';
- width: 40px;
- display: inline-block;
- text-align: right;
- padding-right: 1ex;
- color: #666;
- font-size: 75%
- }
-
- #menu-search-results ul {
- padding: 0 5px;
- margin: 0;
- }
-
- #menu-search-results li {
- white-space: nowrap;
- text-overflow: ellipsis;
- }
-
-
- #menu-trace-list {
- counter-reset: item;
- margin: 0 0 0 20px;
- padding: 0;
- }
- #menu-trace-list li {
- display: block;
- white-space: nowrap;
- }
-
- #menu-trace-list li .secnum:after {
- content: " ";
- }
- #menu-trace-list li:before {
- content: counter(item) " ";
- background-color: #222;
- counter-increment: item;
- color: #999;
- width: 20px;
- height: 20px;
- line-height: 20px;
- display: inline-block;
- text-align: center;
- margin: 2px 4px 2px 0;
- }
-
- @media (max-width: 1000px) {
- body {
- margin: 0;
- display: block;
- }
-
- #menu {
- display: none;
- padding-top: 3em;
- width: 450px;
- }
-
- #menu.active {
- position: fixed;
- height: 100%;
- left: 0;
- top: 0;
- right: 300px;
- }
-
- #menu-toggle {
- visibility: visible;
- }
-
- #spec-container {
- padding: 0 5px;
- }
- }
-
- @media only screen and (max-width: 800px) {
- #menu {
- width: 100%;
- }
-
- h1 .secnum:empty {
- margin: 0; padding: 0;
- }
- }
|