body {
  background: #ffffc0
}

body, p, th, td, caption, h1, h2, h3, ul, ol, dl {
  color: black;
  font-family: sans-serif
}

div {
  margin: 0 0 0 0px;
  padding: 0 0 0 0;
}

div.header {
  margin-bottom: 0px;
}

div.title {
  font-weight: bold;
  font-size: 14px;
  color: #005A9C;
}

div.focushint {
  text-align: right;
  font-size: 10px;
  color: #005A9C;
}

tt, span.keyword, pre {
  font-family: Courier, monospace
}

body, p, th, td, caption, ul, ol, dl, tt, span.kw, pre {
  font-size: 14px
}

A:link {
  color: blue
}

A:visited {
  color: darkblue
}

A:active {
  color: red
}

A {
  text-decoration: none
}

A:hover {
  text-decoration: underline
}

h1, h2, td.h2 {
  color: #005A9C
}

/* Especially for Netscape on Linux: */
h3, td.h3 {
  font-size: 12pt
}

/* identifier in source fragments */
span.identifier {

}

/* symbols in source fragments */
span.symbol {
  color: darkred
}

/* keywords in source fragments */
span.keyword {
  font-weight: bold
}

/* comments in source fragments */
span.comment {
  color: darkcyan;
  font-style: italic;
  font-family: monospace;
}

/* directives in source fragments */
span.directive {
  color: darkyellow;
  font-style: italic
}

/* numbers in source fragments */
span.number {
  color: darkmagenta
}

/* characters (#...) in source fragments */
span.character {
  color: darkcyan
}

/* strings in source fragments */
span.string {
  color: blue
}

/* assembler passages in source fragments */
span.assembler {
  color: green
}


td.pre {
  white-space: pre
}

p.cmt {
  color: gray
}

span.warning {
  color: red;
  font-weight: bold
}

span.file {
  color: darkgreen
}

table.remark {
  background-color: #ffffc0;
}

table.bar {
  background-color: #a0c0ff;
}

span.bartitle {
  font-weight: bold;
  font-style: italic;
  color: darkblue
}

/* definition list */
dl {
  border: 3px double #ccc;
  padding: 0.5em;
}

/* definition list: term */
dt {
  float: left;
  clear: left;
  width: auto; /* normally browsers default width of largest item */
  padding-right: 20px;
  font-weight: bold;
  color: darkgreen;
}

/* definition list: description */
dd {
  margin: 0 0 0 110px;
  padding: 0 0 0.5em 0;
}