Added CSS for docs.

docs/docstyle.css

@@ -0,0 +1,84 @@
+body {
+  background-color: #ffffff;
+  color: black;
+  margin-right: 10%;
+  margin-left: 10%;
+}
+
+h1, h2, h3, h4, h5, h6 {
+  /* Dark sea green: color: #298859;  */
+  /* Design Doc Blue */
+  color: #3366ff;
+  font-family: sans-serif;
+}
+@media print {
+  /* Darker version for printing */
+  h1, h2, h3, h4, h5, h6 {
+    color: #000080;
+    font-family: helvetica, sans-serif;
+  }
+  /* Print out hrefs of links, instead of underlining them */
+  a {
+    text-decoration: none;
+    color: black;
+  }
+  a[href]:after {
+    content: " [" attr(href) "] ";
+    font: normal smaller monospace;
+  }
+}
+
+h1 {
+  text-align: center;
+}
+h2 {
+  margin-left: -0.5in;
+}
+h3 {
+  margin-left: -0.25in;
+}
+h4 {
+  margin-left: -0.125in;
+}
+hr {
+  margin-left: -1in;
+}
+address {
+  text-align: right;
+}
+code,pre,samp,var {
+  color: #006000;
+}
+kbd {
+  color: #600000;
+}
+div.note p {
+  float: right;
+  width: 3in;
+  margin-right: 0%;
+  padding: 1px;
+  border: 2px solid #6060a0;
+  background-color: #fffff0;
+}
+
+pre.code {
+  background-color: #FFFFEE;
+  border: 1px solid black;
+  color: #004000;
+  font-size: 10pt;
+  font-weight: bold;
+  margin-left: 2mm;
+  margin-right: 2mm;
+  padding: 2mm;
+  -moz-border-radius: 12px 0px 0px 0px;
+}
+
+@media print {
+  .str { color: #060; }
+  .kwd { color: #006; font-weight: bold; }
+  .com { color: #600; font-style: italic; }
+  .typ { color: #404; font-weight: bold; }
+  .lit { color: #044; }
+  .pun { color: #440; }
+  .pln { color: #000; }
+}

docs/guidestyle.css

@@ -0,0 +1,58 @@
+
+body {
+  background-color: #ffffff;
+  color: black;
+  margin-right: 1in;
+  margin-left: 1in;
+}
+
+h1, h2, h3, h4, h5, h6 {
+  color: #3366ff;
+  font-family: sans-serif;
+}
+
+h1 {
+  text-align: center;
+  font-size: 18pt;
+}
+h2 {
+  margin-left: -0.5in;
+  margin-top: 0.5in;
+}
+h3 {
+  margin-left: -0.25in;
+}
+h4 {
+  margin-left: -0.125in;
+}
+hr {
+  margin-left: -1in;
+}
+
+.h2toc {
+  font-size: 12pt;
+  color: #3366ff;
+  font-weight: bold;
+  margin-left: 0.5in;
+  line-height: 200%;
+}
+
+.h3toc {
+  font-size: 11pt;
+  color: #3366ff;
+  font-weight: normal;
+  margin-left: 1in;
+}
+
+/* Use the <code> tag for bits of code and <var> for variables and objects. */
+code,pre,samp,var {
+  color: #006000;
+}
+
+.badcode {
+  color: #CC0000;
+}
+
+address {
+  text-align: right;
+}