website/source/user-guide.css

   1 /* @group toc */
   2
   3 .table-of-contents {
   4         font-size: 90%;
   5         margin-bottom: 1em;
   6         padding-bottom: 1em;
   7 }
   8
   9 .table-of-contents h2, h3, h4 {
  10         padding-top: 0;
  11         padding-bottom: 0;
  12         margin-top: 0;
  13         margin-bottom: 1px;
  14 }
  15
  16 .table-of-contents h2 {
  17         font-size: inherit;
  18         font-style: inherit;
  19         position: relative;
  20         left: 2em;
  21 }
  22
  23 .table-of-contents h3 {
  24         font-size: inherit;
  25         font-style: inherit;
  26         position: relative;
  27         left: 4em;
  28 }
  29
  30 .table-of-contents h4 {
  31         font-size: inherit;
  32         font-style: inherit;
  33         position: relative;
  34         left: 6em;
  35 }
  36
  37 .table-of-contents h5 {
  38         font-size: inherit;
  39         font-style: inherit;
  40         position: relative;
  41         left: 8px;
  42 }
  43
  44 /* @end */
  45
  46 /* @group anchors */
  47
  48 a.none {
  49         text-decoration: none;
  50         color:black }
  51
  52 a.none:visited { text-decoration: none; color:black }
  53
  54 a.none:active { text-decoration: none; color:black }
  55
  56 a.none:hover { text-decoration: none; color:black }
  57
  58 a {
  59         text-decoration: none;
  60         }
  61
  62 a:visited {
  63         text-decoration: none;
  64 }
  65
  66 a:active {
  67         text-decoration: underline;
  68 }
  69
  70 a:hover {
  71         text-decoration: underline;
  72 }
  73
  74 /* @end */
  75
  76 /* @group Reference */
  77
  78 .reference {
  79         padding-bottom: 1em;
  80 }
  81
  82 .reference h3 {
  83         margin-top: 2em;
  84         font-size: 110%;
  85         border-bottom: 1px solid silver;
  86         border-top: 4px solid gray;
  87         padding-top: 3px;
  88         padding-bottom: 3px;
  89 }
  90
  91
  92
  93 /* @end */
  94
  95 body {
  96   font-family: Georgia, "Times New Roman", Times, serif;
  97         margin-right: 0.5in;
  98         margin-left: 0.5in;
  99         margin-bottom: 0.25px;
 100 }
 101
 102 h1, h2, h3, h4 {
 103   font-family: "Lucida Grande", Lucida, Verdana, sans-serif;
 104 }
 105
 106 h2 {
 107 }
 108
 109 h3, h4 {
 110         font-style: italic;
 111 }
 112
 113 .hidden {
 114         visibility: hidden;
 115 }
 116
 117 .documentation {
 118         margin-right: 1em;
 119         margin-left: 1em;
 120 }
 121
 122 .function {
 123
 124 }
 125
 126 .documentation.header {
 127         display: block;
 128         position: relative;
 129         border-top-style: solid;
 130         border-top-width: 1pt;
 131         padding-top: 4px;
 132         margin-top: 2em;
 133 }
 134
 135 .documentation.contents {
 136         top: 10px;
 137         position: relative;
 138 }
 139
 140 .documentation-name {
 141         font-weight: bold;
 142         float: left;
 143         padding-right: 10px;
 144         width: 125px;
 145 }
 146
 147 .documentation-kind {
 148         float: right;
 149         font-style: italic;
 150         color: gray;
 151         padding-left: 10px;
 152 }
 153
 154 .documentation-arguments {
 155         float: left;
 156         width: 350px;
 157         font-style: italic;
 158 }
 159
 160 .documentation p {
 161         clear: both;
 162         margin-right: 1em;
 163         margin-left: 1em;
 164 }
 165
 166 pre {
 167         background-color: #ffc8ff;
 168         overflow: auto;
 169         padding-bottom: 5px;
 170         margin-right: 1cm;
 171         margin-left: 1cm;
 172         font-family: "Courier New", Courier, mono;
 173 }
 174
 175 .note {
 176         border: 2px inset gray;
 177         padding: 0.5em;
 178         margin-right: 2em;
 179         margin-left: 2em;
 180 }
 181
 182 #footer {
 183         margin-top: 2em;
 184         border-top-style: inset;
 185         border-top-width: 2px;
 186 }
 187 #navigation li {
 188         display: inline;
 189         border-right-style: dotted;
 190         border-right-width: 1px;
 191         border-left-style: dotted;
 192         border-left-width: 1px;
 193         border-collapse: collapse;
 194         padding-right: 0.25em;
 195         padding-left: 0.25em;
 196         margin-right: 1em;
 197 }
 198
 199 #navigation {
 200         text-align: center;
 201 }
 202
 203 #timestamp {
 204         font-size: 80%;
 205         text-align: right;
 206 }
 207