code, .code {
  font-size: 100%;
  font-family: monospace;
  color:#007000;
}

kbd {
  font-size: 100%;
  font-family: 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: #f8f8ff;
  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;
  }
}