font-size: 10pt;
}
+/* Argh .. doxygen.css has font-size:90% for td ... */
+td {
+ font-size: 100%;
+}
+
#head {
height: 62px;
border-top: 5px solid #DECD40;
padding-bottom: 6px;
}
-div.tabs ul li a:hover, div.tabs ul li.current a {
+div.tabs ul li a:hover, div.tabs ul li.current a, div.tabs ul.glossary li a:hover {
color: #726921;
text-decoration: none;
background-color: #EDE497;
font-size: 90%;
}
+div.tabs ul.glossary li a {
+ background-color: #FDF7C3;
+}
+
+div.tabs ul.glossary li.glossary a {
+ background-color: #EDE497;
+}
+
#footer {
clear: both;
padding: 4px 10px 4px 142px;
font-weight: bold;
}
+table.fixedcolumn td:first-child {
+ width: 35%;
+}
+
table.ebnf {
margin: 0;
padding: 0;
border-spacing: 0;
border: none;
- font-size: 120%; /* ???????? Why is THIS needed ?? */
}
table.ebnf td {
padding: 0;
border-spacing: 0;
border: none;
- font-size: 120%; /* ???????? Why is THIS needed ?? */
}
table.listing td {
text-indent: -4em;
}
+#autotoc h1 {
+ font-size: 120%;
+ text-align: left;
+}
+
+#autotoc ul {
+ list-style-type: none;
+ padding: 0;
+ margin: 1em 0 1em 2em;
+}
+
+#autotoc ul li.level_h2 {
+ margin: .5em 0 .2em 0;
+}
+
+#autotoc ul li.level_h3 {
+ margin-left: 1.5em;
+}
+
+#autotoc ul li.level_h4 {
+ margin-left: 3em;
+}
+
/* \f
* Local Variables:
* indent-tabs-mode: nil