235 lines
5.6 KiB
CSS
235 lines
5.6 KiB
CSS
body {
|
|
font-size: 18px;
|
|
line-height: 1.5;
|
|
font-family: Cambria, Palatino Linotype, Palatino, Liberation Serif, serif;
|
|
margin: 0 20%;
|
|
color: #333;
|
|
}
|
|
|
|
a:link {
|
|
text-decoration: none;
|
|
color: #3333bb;
|
|
}
|
|
|
|
a:hover {
|
|
text-decoration: underline;
|
|
color: blue;
|
|
}
|
|
|
|
a:visited {
|
|
color: inherit;
|
|
}
|
|
|
|
code {
|
|
font-weight: bold;
|
|
font-family: Consolas, Monaco, monospace;
|
|
white-space: pre;
|
|
}
|
|
|
|
pre code {
|
|
font-weight: inherit;
|
|
}
|
|
|
|
pre code.hljs {
|
|
background-color: #fff;
|
|
}
|
|
|
|
ol.toc {
|
|
list-style: none;
|
|
padding-left: 0;
|
|
}
|
|
|
|
ol.toc ol.toc {
|
|
padding-left: 2ex;
|
|
list-style: none;
|
|
}
|
|
|
|
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-note {
|
|
display: block;
|
|
margin-left: 5em;
|
|
color: #666;
|
|
}
|
|
|
|
emu-note span.note {
|
|
text-transform: uppercase;
|
|
margin-left: -5em;
|
|
display: block;
|
|
float: left;
|
|
}
|
|
|
|
emu-production {
|
|
display: block;
|
|
margin-top: 1em;
|
|
margin-bottom: 1em;
|
|
margin-left: 5ex;
|
|
}
|
|
|
|
emu-production.inline {
|
|
display: inline;
|
|
margin: 0;
|
|
}
|
|
|
|
emu-production.inline 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 {
|
|
font-style: italic;
|
|
}
|
|
|
|
emu-rhs emu-nt {
|
|
margin-right: 1ex;
|
|
}
|
|
|
|
emu-t {
|
|
font-family: monospace;
|
|
font-weight: bold;
|
|
margin-right: 1ex;
|
|
}
|
|
|
|
emu-rhs {
|
|
display: block;
|
|
padding-left: 50px;
|
|
}
|
|
|
|
emu-mods {
|
|
font-size: .75em;
|
|
vertical-align: sub;
|
|
font-style: normal;
|
|
}
|
|
|
|
emu-gprose {
|
|
font-size: 0.9em;
|
|
font-family: Helvetica, Arial, sans-serif;
|
|
}
|
|
|
|
h1, h2, h3, h4, h5, h6 {
|
|
position: relative;
|
|
}
|
|
h1 .secnum {
|
|
position: absolute;
|
|
text-align: right;
|
|
right: 100%;
|
|
margin-right: 1ex;
|
|
white-space: nowrap;
|
|
}
|
|
|
|
h1 { font-size: 2.67em; }
|
|
h2 { font-size: 2em; }
|
|
h3 { font-size: 1.56em; }
|
|
h4 { font-size: 1.25em; }
|
|
h5 { font-size: 1.11em; }
|
|
h6 { font-size: 1em; }
|
|
|
|
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;
|
|
}
|
|
|
|
table.real-table {
|
|
border-collapse: collapse;
|
|
}
|
|
table.real-table td, table.real-table th {
|
|
border: 1px solid black;
|
|
padding: 0.4em;
|
|
vertical-align: baseline;
|
|
}
|
|
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;
|
|
}
|
|
|