1 files changed, 92 insertions, 0 deletions
diff --git a/docs/manual/style.css b/docs/manual/style.css
new file mode 100644
index 0000000..28fc112
--- /dev/null
+++ b/docs/manual/style.css
@@ -0,0 +1,92 @@
+@charset "iso-8859-1";
+
+/* Global settings. */
+
+body {
+  background: #FFFFFF;
+}
+
+h1 {
+  text-align: center;
+}
+
+h2 {
+  background: #EEEEFF;
+  padding: 10px;
+}
+
+dt {
+  padding: 6px;
+}
+
+dt div 
+{
+  color: grey;
+  float: right;
+}
+
+dd {
+  padding: 6px;
+}
+
+pre {
+  padding: 10px;
+  background: #E0E0E0;
+}
+
+a
+{
+  text-decoration: none;
+}
+
+/* Settings for variable width code. */
+
+p.code {
+  padding: 10px;
+  background: #E0E0E0;
+}
+
+
+/* Settings for diagrams. */
+
+table.diagram {
+  padding: 8px;
+  border: none;
+  border-spacing: 2px;
+}
+
+td.transparentblock {
+  text-align: center;
+  padding: 10px 0px;
+}
+
+td.whiteblock {
+  width: 100px;
+  text-align: center;
+  border: solid #C0C0C0 1px;
+  background: #E0E0E0;
+  padding: 10px 0px;
+}
+
+td.lightblock {
+  width: 100px;
+  text-align: center;
+  border: solid #8888FF 1px;
+  background: #BBBBFF;
+  padding: 20px 0px;
+}
+
+td.darkblock {
+  width: 100px;
+  text-align: center;
+  background: #8888FF;
+  padding: 20px 0px;
+}
+
+/* Settings for buttons. */
+
+td.button {
+  background: #E0E0E0;
+  border: outset #FFFFFF 1px;
+  font-weight: bold;
+}