1 html { 2 padding:0px; 3 margin:0px; 4 } 5 6 body { 7 background-color: #fff; 8 font-family: Verdana, Arial, SunSans-Regular, Sans-Serif; 9 color: #000; 10 padding:0px; 11 margin:0px; 12 font-size: small; 13 } 14 15 #job img { border:1px solid #DDDDDD; } 16 #job:hover img { border:1px solid #8888EE; } 17 18 p, h2, pre { 19 margin: 0px; 20 padding-top: 5px; 21 padding-bottom: 5px; 22 /*padding-left: 1ex;*/ 23 /*padding: 5px 20px 5px 20px; */ 24 } 25 26 p.rm { 27 padding-top: 0px; 28 padding-bottom: 0px; 29 } 30 31 a { 32 color: #4183c4; 33 /*font-size: smaller;*/ 34 background-color:transparent; 35 text-decoration: none; 36 } 37 38 #content a:hover { 39 text-decoration: underline; 40 } 41 42 .source { 43 border-top: 1px solid #DDDDDD; 44 border-bottom: 1px solid #DDDDDD; 45 background:#f5f5f5; 46 font-family: Courier, "MS Courier New", Prestige, Everson Monocourrier, monospace; 47 padding-bottom: 0.5ex; 48 padding-top: 0.5ex; 49 padding-left: 1ex; 50 51 margin-left: 0ex; 52 margin-top: 0.5ex; 53 margin-bottom: 0.5ex; 54 white-space: pre; 55 56 -webkit-border-radius: 3px; 57 -moz-border-radius: 3px; 58 border-radius: 3px; 59 } 60 61 pre { 62 background-color:transparent; 63 font-family: Monaco, Andale Mono, Courier New, monospace; 64 } 65 66 .alignright { 67 margin-top: 0; 68 text-align: right; 69 font-size: 10px; 70 } 71 72 h1, h2, h3, h4 { 73 color: #333; 74 } 75 76 h2 { 77 padding-top:10px; 78 background-color: transparent; 79 font-weight: 900; 80 font-size: x-large; 81 } 82 83 h3 { 84 padding-top: 5px; 85 background-color: transparent; 86 font-weight: normal; 87 font-size: large; 88 } 89 90 h4 { 91 padding-top:5px; 92 background-color: transparent; 93 font-weight: normal; 94 font-size: large; 95 } 96 97 table.footer { 98 width: 100%; 99 } 100 101 .footer { 102 text-align: right; 103 color: #564b47; 104 background-color: #fff; 105 padding:0px; 106 border-top: 1px solid #CCCCCC; 107 margin-top: 3ex; 108 font-size: smaller; 109 } 110 111 112 strong { 113 /*font-size: 13px;*/ 114 font-weight: bold; 115 } 116 117 /* positioning-layers static and absolute */ 118 119 #breadcrumbs { 120 padding: 3px 10px 3px 10px; 121 margin: 0px 4px 0px 4px; 122 font-size: small; 123 border: 1px solid #CCCCCC; 124 /*border-bottom: 1px solid #aaa; 125 /* background-color: #ccc; lime; 126 border-color: #663300;*/ 127 background-color: #ffd0a0; 128 /*max-width: 77em;*/ 129 } 130 131 #left { 132 position: absolute; 133 left: 0px; 134 width: 15em; 135 margin: 4px 0px 0px 4px; 136 padding: 0px; 137 font-size: 80%; 138 background-color: #ffffff; 139 } 140 141 .menuGroup { 142 border: 1px solid #cccccc; 143 background-color: #fff8e8; 144 color: #564b47; 145 border: 1px solid #cccccc; 146 -webkit-border-radius: 3px; 147 -moz-border-radius: 3px; 148 border-radius: 3px; 149 } 150 151 .menuGroup a { 152 display: block; 153 width: 95.5%; 154 margin: 0px; 155 padding: 2px; 156 border: solid 1px #fff8e8; 157 color: #0066cc; 158 text-decoration: none; 159 } 160 161 .menuGroup a:hover { 162 border: solid 1px #FFFFFF; 163 background-color: #3333CC; 164 color: #ffffff; 165 -webkit-border-radius: 3px; 166 -moz-border-radius: 3px; 167 border-radius: 3px; 168 } 169 170 .pub { 171 text-align: center; 172 } 173 174 #left .pub a:hover { 175 background-color: transparent; 176 border: solid 0px #FFFFFF; 177 } 178 179 #left a:hover, #right a:hover { 180 border: solid 1px #FFFFFF; 181 background-color: #3333CC; 182 color: #ffffff; 183 -webkit-border-radius: 3px; 184 -moz-border-radius: 3px; 185 border-radius: 3px; 186 } 187 188 #left div.jobadd { 189 font-size: 160%; 190 color: #fff; 191 margin: 0px; 192 padding: 1ex; 193 194 text-align: center; 195 -webkit-border-radius: 3px; 196 -moz-border-radius: 3px; 197 border-radius: 3px; 198 199 background-image: -ms-linear-gradient(bottom right, #FFBB55 0%, #FF8822 100%); 200 background-image: -moz-linear-gradient(bottom right, #FFBB55 0%, #FF8822 100%); 201 background-image: -o-linear-gradient(bottom right, #FFBB55 0%, #FF8822 100%); 202 background-image: -webkit-gradient(linear, right bottom, left top, color-stop(0, #FFBB55), color-stop(1, #FF8822)); 203 background-image: -webkit-linear-gradient(bottom right, #FFBB55 0%, #FF8822 100%); 204 background-image: linear-gradient(to top left, #FFBB55 0%, #FF8822 100%); 205 } 206 207 #left div.jobadd a, div.jobadd a:hover { 208 background-color: transparent; 209 color: #fff; 210 border-width: 0px; 211 } 212 213 p.menu_header { 214 margin: 0px; 215 padding: 2px; 216 font-weight: normal; 217 background-color: #ffd0a0; 218 border-top: solid 1px #CCCCCC; 219 border-bottom: solid 1px #CCCCCC; 220 } 221 222 #content { 223 margin: 0px 12em 0px 16em; 224 padding: 0px; 225 background-color: #ffffff; 226 } 227 228 229 #content img { 230 border:none; 231 margin-left: auto; 232 margin-right: auto; 233 display: block; 234 } 235 236 .author { 237 text-align: left; 238 font-weight: bold; 239 } 240 241 .definition { 242 padding-left: 5px; 243 padding-right: 5px; 244 margin: 5px 50px 5px 50px; 245 text-align: justify; 246 background-color: #E6E64C; 247 } 248 249 .deftitle { 250 font-weight: bold; 251 } 252 253 .big { 254 font-size: 130%; 255 } 256 257 .green { 258 color: green; 259 } 260 .blue { 261 color: blue; 262 } 263 264 .red { 265 color: red; 266 } 267 268 .bold { 269 font-weight: bold; 270 } 271 272 .redBold { 273 color: red; 274 font-weight: bold; 275 } 276 .greenBold { 277 color: green; 278 font-weight: bold; 279 } 280 281 code { 282 font-family: Courier, monospace; 283 } 284 285 286 .option { 287 border: 1px solid black; 288 font-family: Arial, sans-serif; 289 } 290 .highlight { 291 width: 18em; 292 float: right; 293 display: inline; 294 font-size: 110%; 295 296 border: 2px solid #711; 297 -webkit-border-radius: 4px; 298 -moz-border-radius: 4px; 299 border-radius: 4px; 300 background:#FFE0B0; 301 padding-top: 1ex; 302 padding-left: 1ex; 303 padding-right: 1ex; 304 padding-bottom: 1ex; 305 margin-left: 1em; 306 margin-right: 0em; 307 margin-bottom: 1ex; 308 } 309 310 311 .survey { 312 font-weight: bolder; 313 font-size: larger; 314 315 border:1px solid #cccccc; 316 background:#FFCC99; 317 padding-left: 1ex; 318 padding-right: 1ex; 319 } 320 /* ========== body table ============ */ 321 table.bodyTable { 322 padding: 0px; 323 margin-left: -2px; 324 margin-right: -2px; 325 } 326 327 table.bodyTable th { 328 color: white; 329 background-color: #bbb; 330 font-weight: bold; 331 } 332 333 334 table.bodyTable td { 335 padding-left: 0.5ex; 336 padding-bottom: 0.5ex; 337 } 338 339 340 /* apply to tr elements of tables which are both bodytable and dark */ 341 table[class="bodyTable dark"] tr { 342 background-color: #ddd; 343 } 344 345 /* apply to tr elements of tables which are both bodytable and dark */ 346 table[class="bodyTable properties"] tr { 347 vertical-align: top; 348 } 349 350 table.bodyTable tr.a { 351 background-color: #ddd; 352 } 353 354 table.bodyTable tr.b { 355 background-color: #eee; 356 } 357 358 table.bodyTable tr.alt { 359 background-color: #eee; 360 } 361 362 .striped tr:nth-child(odd) td { 363 background-color: #f9f9f9; 364 } 365 .striped td { 366 background-color: #f0f0f0; 367 } 368 369 /* EOF =============== bodyTable =============== */ 370 371 .label { 372 padding: 1px 3px 2px; 373 font-size: 9.75px; 374 font-weight: bold; 375 color: #ffffff; 376 text-transform: uppercase; 377 white-space: nowrap; 378 background-color: #bfbfbf; 379 -webkit-border-radius: 3px; 380 -moz-border-radius: 3px; 381 border-radius: 3px; 382 } 383 .label.notice { 384 background-color: #62cffc; 385 } 386 387 388 /* ------------------------------------ */ 389 390 dt { 391 border-top: 2px solid #888888; 392 color: #333; 393 padding-bottom: 1ex; 394 padding-top: 1ex; 395 font-weight: bold; 396 } 397 dd { 398 margin-top: 1ex; 399 margin-bottom: 1ex; 400 } 401 402 /* ------------------------------------ */ 403 .anchor { display:none; } 404 405 h1 .anchor:before {content:url(anchor24.png);} 406 h2 .anchor:before {content:url(anchor20.png);} 407 h3 .anchor:before {content:url(anchor16.png);} 408 h4 .anchor:before {content:url(anchor12.png);} 409 td .anchor:before {content:url(anchor12.png);} 410 dt .anchor:before {content:url(anchor12.png);} 411 412 h1:hover .anchor { margin-left: -24px; } 413 h2:hover .anchor { margin-left: -20px; } 414 h3:hover .anchor { margin-left: -16px; } 415 h4:hover .anchor { margin-left: -12px; } 416 td:hover .anchor { margin-left: -12px; } 417 dt:hover .anchor { margin-left: -12px; } 418 419 h1:hover .anchor, 420 h2:hover .anchor, 421 h3:hover .anchor, 422 h4:hover .anchor, 423 td:hover .anchor, 424 dt:hover .anchor { 425 display: inline-block; 426 text-decoration: none; 427 } 428 429 430 /* ------------ twitter button ------- */ 431 .twitter_button { 432 vertical-align: text-bottom; 433 padding-top: 3px; 434 padding-right: 16px; 435 float: left; 436 height: 18px;div 437 text-shadow: 0 1px 0 rgba(255, 255, 255, 0.5); 438 white-space: nowrap; 439 background-color: white; 440 background-image: -moz-linear-gradient(top, #ffffff, #dedede); 441 background-image: -webkit-gradient(linear, left top, left bottom, from(#ffffff), to(#dedede)); 442 background-image: -ms-linear-gradient(top, #ffffff, #dedede); 443 background-image: linear-gradient(top, #ffffff, #dedede); 444 background-image: -o-linear-gradient(top, #ffffff, #dedede); 445 border: #CCC solid 1px; 446 -webkit-border-radius: 3px; 447 -moz-border-radius: 3px; 448 border-radius: 3px; 449 } 450