body {
  margin: 10px;
  padding: 10px;
}

pre.docstring {
  margin: 20px;
}

div.symbol {
  padding:2px;
  background-color:#ddeeee;
}

div.kind {
  padding:2px;
  background-color:#ddeeee;
}

.undocumented {
  foreground-color:#ff0000;
}

.menu a {
  background-color:#80a0a0;
  border:1px solid #308080;
  padding:2px;
}

.menu input {
  color:#000000;
  background-color:#80a0a0;
  border:1px solid #308080;
  padding:2px;
}

.menu a:link    {color:#000000;}  /* unvisited link */
.menu a:visited {color:#004444;}  /* visited link */
.menu a:hover   {color:#FFFFFF;}  /* mouse over link */
.menu a:active  {color:#00FFFF;}  /* selected link */

.header p { font-size:80%; }
.footer p { font-size:80%; }