added a quick reference section

1 files changed, 53 insertions, 2 deletions

diff --git a/htdocs/style.css b/htdocs/style.css
index 83e308f..96e4c59 100644
--- a/htdocs/style.css
+++ b/htdocs/style.css
@@ -1,17 +1,17 @@
 body {
  font-family: sans-serif;
  font-size: 11pt;
 }
 
-a {
+a:link, a:visited {
  text-decoration: none;
 }
-a:hover {
+a:link:hover, a:visited:hover {
  text-decoration: underline;
 }
 p {
  margin: 1ex 1em;
  text-indent: 2em;
  text-align: justify;
 }
 p.note {
@@ -19,16 +19,17 @@ p.note {
  border-width: 1px 1px 1px 6px;
  border-color: gray gray gray #0000a0;
  border-style: solid solid solid double;
  padding: 1ex 1ex 1ex 2em;
  font-size: 80%;
  background: #c0c0e0;
  color: #202020;
 }
+code a,
 code {
  color: #d04040;
 }
 em {
  white-space: nowrap;
 }
 
 div.google_ad {
@@ -113,19 +114,30 @@ div#sidepanel div.copyright {
 div#content h1 {
  font-size: 140%;
  color: gray;
  font-weight: bold;
  text-align: center;
  margin: 1em;
  clear: both;
 }
+div#content h2 {
+ font-size: 140%;
+ color: #8080a0;
+ font-weight: bold;
+ text-align: center;
+ margin: 1em;
+ clear: both;
+}
 div#content p a {
  font-weight: bold;
 }
+div#content p a.internal {
+ font-weight: inherit !important;
+}
 
 div.insert {
  text-align: center;
 }
 iframe#insert {
  border: 1px solid black;
 }
 
@@ -198,8 +210,47 @@ div.prevnext a.prevnext-next {
  float: right;
  text-align: right;
 }
 div.prevnext a:hover {
  background: gray;
  border: black 1px solid;
  color: white;
 }
+
+ul.quickref.toc {
+ margin: 1em 20%;
+ font-size: 90%;
+ border: solid 1px gray;
+}
+
+dl.quickref {
+ margin: 1ex 1em;
+}
+dl.quickref dt {
+ margin: 0.4ex;
+ padding: 2px 0.5ex;
+ background: #e0e0e0;
+ display: compact;
+}
+dl.quickref dd {
+ margin: 0px 0.4ex 0.4ex 10%;
+ padding: 0px;
+ border: 1px solid grey;
+}
+dl.quickref code kbd {
+ font-style: italic;
+ color: #0000c0;
+}
+dl.quickref blockquote {
+ background: #ffffc0;
+ padding: 4px;
+ border: dotted 1px gray;
+ font-family: monospace;
+}
+dl.quickref blockquote em {
+ display: block;
+ font-family: inherit !important;
+ font-size: inherit !important;
+ font-weight: inherit !important;
+ font-style: inherit !important;
+ background: #ffc0c0;
+}