body {
  font-family: Verdana, Geneva, Arial, sans-serif;
}
h1, h2, h3, h4, h5, h6 {
  color: gray;
}
#footer {
  font-size: 66%;
  text-align: center;
  margin-top: 20px;
  background-color: #DDDDDD;
}

img {
  border-style: solid;
  border-width: 1px;
}

#menu {
  float: left;
  clear: left;
  width: 180px;
  padding-right: 20px;
}
#menu li {
  list-style-type: none;
  margin-bottom: 10px;
  margin-left: -18px;
}
#menu li a {
  list-style-type: none;
  border : 1px solid black;
  display: block;
  padding: 4px 15px 4px 15px;
  text-decoration: none;
}
#menu li a:link {
  color: white;
  background: rgb(60%, 60%, 90%);
}
#menu li a:visited {
  color: white;
  background: rgb(60%, 60%, 90%);
}
#menu li a:hover {
  color: gray;
  background: rgb(90%, 90%, 20%);
}
#menu li a#current {
  color: gray;
  background: rgb(90%, 90%, 20%);
}
#menu ul.submenu li a {
  font-size: small;
  background: rgb(70%, 70%, 90%);
}
#menu ul.submenu li a:hover {
  color: black;
}
#main {
  margin-left: 220px;
  margin-right: 10%;
  line-height: 1.6em;
}
#main a:link {
  color: blue;
  text-decoration: none;
  border-bottom: thin dotted blue;
}
#main a:visited {
  color: gray;
  text-decoration: none;
  border-bottom: thin dotted gray;
}
#main a:hover {
  background: rgb(90%, 90%, 20%);
}

#examplesketch {
  text-align: center;
}
#examplesketch img {
  border: none;
  display: inline;
  margin: 5px 0px;
}
#examplesketch a:link, #examplesketch a:hover {
  text-decoration: none;
  border: none;
  background: none;
}

pre {
  line-height: 1.3em;
}
pre.code {
  line-height: 1.3em;
  background-color: #DDDDDD;
  padding: 15px;
}

/* Figure environment for library documentation. */
div.figure {
  position: relative;
  width: 650px;
  margin: 20px auto;
  background-color: white;
  line-height: 1em;
}
div.figure p {
  text-align: center;
/*  font-style: italic; */
  font-size: smaller;
  text-indent: 0;
  margin:0px;
}
div.figure img {
  border: thin solid black;
  padding: 10px;
  margin: 0px;
}
div.figure img.noborder {
  border: none;
  padding: 0px;
}
div.figure div.subfigure {
  width: 300px;
  float: left;
  margin:12px;
}
div.ref {
  font-size: small;
  color: #444;
  line-height: 1.1em;
}
ul.pubs li {
  margin-top: 10px;
  line-height: 1.2em;
}

/* Docs */
div.sect1 {
  font-family: monospace;
}

div.sectionbody p {
  white-space: pre;
}

div.sect1 ul li p {
  white-space: normal;
}
div.sect1 dl dd p {
  margin-top: -24px;
}