font-weight: bold;
}
+table.ebnf {
+ margin: 0;
+ padding: 0;
+ border-spacing: 0;
+ border: none;
+ font-size: 120%; /* ???????? Why is THIS needed ?? */
+}
+
+table.ebnf td {
+ text-align: left;
+ border: none;
+ padding: 0;
+}
+
+table.ebnf td:first-child {
+ width: 1%;
+ padding-right: 1ex;
+ font-style: italic;
+}
+
dl.xref-bug, dl.xref-fix, dl.xref-todo, dl.xref-idea {
border: 1px solid #CC8888;
padding: 2px 3px;
width: 35%;
}
+div.toc {
+ width: 25%;
+ margin: 10px 0px;
+}
+
+div.toc ol {
+ padding: 0px;
+ margin: 0pt 0pt 0pt 40px;
+ list-style-type: decimal;
+}
+
+div.toc li {
+ padding: none;
+}
+
+div.toc div {
+ margin: 10px 0px;
+ font-weight: bold;
+ font-size: 120%
+}
+
/* \f
* Local Variables:
* indent-tabs-mode: nil