9 .table-of-contents h2, h3, h4 {
16 .table-of-contents h2 {
23 .table-of-contents h3 {
30 .table-of-contents h4 {
37 .table-of-contents h5 {
49 text-decoration: none;
52 a.none:visited { text-decoration: none; color:black }
54 a.none:active { text-decoration: none; color:black }
56 a.none:hover { text-decoration: none; color:black }
59 text-decoration: none;
63 text-decoration: none;
67 text-decoration: underline;
71 text-decoration: underline;
76 /* @group Reference */
85 border-bottom: 1px solid silver;
86 border-top: 4px solid gray;
96 font-family: Georgia, "Times New Roman", Times, serif;
99 margin-bottom: 0.25px;
103 font-family: "Lucida Grande", Lucida, Verdana, sans-serif;
126 .documentation.header {
128 background-color: lightgrey;
136 padding: 1mm 1mm 1mm 1em;
140 .documentation.contents {
145 .documentation-name {
152 .documentation-kind {
159 .documentation-arguments {
172 background-color: #ffc8ff;
177 font-family: "Courier New", Courier, mono;
181 border: 2px inset gray;
189 border-top-style: inset;
190 border-top-width: 2px;
194 border-right-style: dotted;
195 border-right-width: 1px;
196 border-left-style: dotted;
197 border-left-width: 1px;
198 border-collapse: collapse;
199 padding-right: 0.25em;
200 padding-left: 0.25em;