blob: a86ab931033c7b88031ab9c075f2917038fe97c1 [file] [log] [blame]
code, .code {
font-size: 9pt;
font-family: Courier, Courier New, monospace;
color:#007000;
}
kbd {
font-family: Courier, Courier New, monospace;
font-weight: bold;
}
pre.ebnf {
background-color: beige;
}
pre.grammar {
background-color: beige;
}
p.rule {
font-style: italic
}
span.event {
font-style: italic
}
body {
font: 13px Helvetica, Arial, sans-serif;
}
h1, h2, h3, h4, h5, h6 {
font-family: Helvetica, Arial, sans-serif;
margin-bottom: 0.25em;
}
h2 {
background-color: #e5ecf9;
margin-top: 2em;
border-top:1px solid #36C;
}
pre{
font-size: 9pt;
background-color: #fafaff;
margin: 1em 0 0 0;
padding: .99em;
line-height: 125%;
overflow: auto;
word-wrap: break-word;
}
li {
padding-bottom: 0.5em;
}
li pre {
margin: 0.5em 0px 1em 0px;
}
/* Above this comment, styles meant to help page authors achieve beauty. */
/* Below this comment, styles used in the boilerplate-ish parts of pages. */
div#content {
margin-left: 20%;
padding: 0 1em 2em 1em;
margin-top: -2px;
border: 2px solid #e5ecf9;
}
#topnav {
margin: 0px;
padding: .1em 0px;
width: 100%;
white-space: nowrap;
background-color: #e5ecf9;
border-top:1px solid #36C;
font: bold large Helvetica, Arial, sans-serif;
}
div#linkList {
font: 13px Helvetica, Arial, sans-serif;
float: left;
width: 20%;
}
div#linkList ul {
padding: 1px;
list-style-type: none;
}
div#linkList li {
margin-left: 1em;
}
div#linkList li.navhead {
font-weight: bold;
margin-left: 0px;
}
#nav dl {
margin: 0 0.5em 0 0.5em;
padding: 0px;
}
.navtop {
font-size: xx-small;
float: right;
}
#footer {
margin: 2em;
text-align: center;
color: #555;
font-size: small;
}
#footer a {
color: #555;
}
@media print {
div#linkList {
display: none;
}
.navtop {
display: none;
}
div#content {
margin-left: 0px;
border: none;
}
}