body {
  margin: 20px;
  font-family: sans-serif;
  background-color: rgb(153, 51, 0);
  /*
  background-image: url(bg.png);
  border-left: 1px solid rgb(0, 0, 100);
  border-right: 1px solid rgb(0, 0, 100);
  */
}

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

div.title {
  text-align: center;
  vertical-align: middle;
  font-size: 36px;
  padding-top: 10px;
  padding-bottom: 10px;
  /*
  border-top: 1px solid rgb(0, 0, 100);
  border-bottom: 1px solid rgb(0, 0, 100);
  background-color: rgb(204, 102, 51);
  */
  background-image: url(bg.png);
  color: white;
}  

div.toc {
  padding: 10px;
  background-color: rgb(255, 223, 199);
}

div.toc-header {
  text-align: left;
  font-size: x-large;
}

div.toc-section {
  font-size: medium;
  padding-top: 2px;
  padding-bottom: 2px;
}

div.toc-subsection {
  font-size: small;
  font-style: italic;
  margin-left: 50px;
  text-indent: -20px;
  padding-bottom: 2px;
}

div.main {
  padding-left: 0px; 
  margin-left: 0px;
  padding-top: 0.5em;
  background-color: rgb(255, 223, 199);
}

div.item {
  margin-left: 20px;
  margin-top: 0.5em;
  margin-bottom: 0.5em;
}

div.example {
  white-space: pre;
  font-family: monospace;
  font-size: large;
  color: rgb(128, 0, 0);
  margin-left: 40px;
  margin-top: 1em;
  margin-bottom: 1em;
  margin-right:20px;
  padding: 5px;
  border: thin solid rgb(255, 160, 160);
  background-color: rgb(255, 240, 200);
}

div.html {
  font-size: medium;
  color: rgb(128, 0, 0);
  margin-left: 40px;
  margin-top: 1em;
  margin-bottom: 1em;
  margin-right:20px;
  padding: 5px;
  border: thin solid rgb(255, 160, 160);
  background-color: rgb(255, 230, 230);
}

div.totop {
  margin-left: 20px;
}

div.plain {
  inherit: none;
}

code {
  white-space: pre;
  font-family: monospace;
  font-size: large;
}

div.section {
  margin-top: 1em;
  margin-bottom: 1em;
}

div.subsection {
  margin-top: 1em;
  margin-bottom: 1em;
}

h1 {
  padding-top: 5px;
  padding-bottom: 5px;
  padding-left: 20px;
  font-size: x-large;
  font-weight: bold;
  /*
  border-top: 1px solid rgb(0, 0, 100);
  border-bottom: 1px solid rgb(0, 0, 100);
  */
  /*
  background-color: rgb(204, 102, 51);
  */
  color: white;
  background-image: url(bg.png);
}

h2 {
  padding-top: 2px;
  padding-bottom: 2px;
  padding-left: 20px;
  font-size: large;
  font-style: italic;
  font-weight: bold;
  /*
  border-top: 1px solid rgb(0, 0, 100);
  border-bottom: 1px solid rgb(0, 0, 100);
  */
  /*
  background-color: rgb(204, 102, 51);
  */
  color: white;
  background-image: url(bg.png);
}

a:link {
  color: black;
}

a:visited {
  color: black;
}

a:hover {
  color: red;
}

td {
  border: thin solid black;
  padding: 2px 5px;
  vertical-align: top;
}

th {
  border: thin solid black;
  text-align: center;
  padding: 5px 2px;
}

table {
  border-collapse: collapse;
  margin-left: 50px;
  margin-right: 10px;
  margin-top: 10px;
  background-color: white;
}

div.html table {
  border-collapse: inherit;
  margin-left: inherit;
  margin-right: inherit;
  margin-top: inherit;
}

div.html table tr td {
  border: inherit;
  padding: inherit;
  vertical-align: inherit;
}

table.code {
  border-collapse: collapse;
  margin-left: 40px;
  margin-right: 5px;
  margin-top: 5px;
  background-color: rgb(255, 240, 200);
}

td.code {
  white-space: pre;
  border: thin solid rgb(255, 160, 160);
  font-family: monospace;
  font-size: large;
  color: rgb(128, 0, 0);
}