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         background-color: lightgrey;
 129         color: black;
 130         position: relative;
 131         padding-top: 4px;
 132         margin-top: 2em;
 133         width:auto;
 134         min-width:120px;
 135         font-size: medium;
 136         padding: 1mm 1mm 1mm 1em;
 137         border: none;
 138 }
 139
 140 .documentation.contents {
 141         top: 10px;
 142         position: relative;
 143 }
 144
 145 .documentation-name {
 146         font-weight: bold;
 147         float: left;
 148         padding-right: 10px;
 149         width: 80%;
 150 }
 151
 152 .documentation-kind {
 153         float: right;
 154         font-style: italic;
 155         color: gray;
 156         padding-left: 10px;
 157 }
 158
 159 .documentation-arguments {
 160         float: left;
 161         width: 350px;
 162         font-style: italic;
 163 }
 164
 165 .documentation p {
 166         clear: both;
 167         margin-right: 1em;
 168         margin-left: 1em;
 169 }
 170
 171 pre {
 172         background-color: #ffc8ff;
 173         overflow: auto;
 174         padding-bottom: 5px;
 175         margin-right: 1cm;
 176         margin-left: 1cm;
 177         font-family: "Courier New", Courier, mono;
 178 }
 179
 180 .note {
 181         border: 2px inset gray;
 182         padding: 0.5em;
 183         margin-right: 2em;
 184         margin-left: 2em;
 185 }
 186
 187 #footer {
 188         margin-top: 2em;
 189         border-top-style: inset;
 190         border-top-width: 2px;
 191 }
 192 #navigation li {
 193         display: inline;
 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;
 201         margin-right: 1em;
 202 }
 203
 204 #navigation {
 205         text-align: center;
 206 }
 207
 208 #timestamp {
 209         font-size: 80%;
 210         text-align: right;
 211 }
 212