Home | History | Annotate | Download | only in manual 
      1 @charset "iso-8859-1";
      2 
      3 /* Global settings. */
      4 
      5 body
      6 {
      7   background: #FFFFFF;
      8 }
      9 
     10 h1
     11 {
     12   text-align: center;
     13 }
     14 
     15 h2
     16 {
     17   background: #EEEEFF;
     18   padding: 10px;
     19 }
     20 
     21 dt
     22 {
     23   padding: 6px;
     24 }
     25 
     26 dt div 
     27 {
     28   color: grey;
     29   float: right;
     30 }
     31 
     32 dd
     33 {
     34   padding: 6px;
     35 }
     36 
     37 pre
     38 {
     39   padding: 10px;
     40   background: #E0E0E0;
     41 }
     42 
     43 .spacious li
     44 {
     45   padding: 8px;
     46 }
     47 
     48 .shifted li
     49 {
     50   margin-left: 50px;
     51 }
     52 
     53 img.float
     54 {
     55   float: left;
     56 }
     57 
     58 a
     59 {
     60   text-decoration: none;
     61 }
     62 
     63 a.button
     64 {
     65   color: #000000;
     66   text-decoration: none;
     67   background: #E0E0E0;
     68   border: 1px outset #FFFFFF;
     69   float: right;
     70 }
     71 
     72 a.largebutton {
     73   font-weight: bold;
     74   color: #000000;
     75   margin: 0px;
     76   padding: 10px;
     77   background: #D0D0D0;
     78   text-decoration: none;
     79   border: 1px outset #FFFFFF;
     80 }
     81 
     82 /* Settings for variable width code. */
     83 
     84 p.code
     85 {
     86   padding: 10px;
     87   background: #E0E0E0;
     88 }
     89 
     90 
     91 /* Settings for diagrams. */
     92 
     93 table.diagram
     94 {
     95   padding: 8px;
     96   border: none;
     97   border-spacing: 2px;
     98 }
     99 
    100 td.transparentblock
    101 {
    102   text-align: center;
    103   padding: 10px 0px;
    104 }
    105 
    106 td.whiteblock
    107 {
    108   width: 100px;
    109   text-align: center;
    110   border: 1px solid #C0C0C0;
    111   background: #E0E0E0;
    112   padding: 10px 0px;
    113 }
    114 
    115 td.lightblock
    116 {
    117   width: 100px;
    118   text-align: center;
    119   border: 1px solid #8888FF;
    120   background: #BBBBFF;
    121   padding: 20px 0px;
    122 }
    123 
    124 td.darkblock
    125 {
    126   width: 100px;
    127   text-align: center;
    128   background: #8888FF;
    129   padding: 20px 0px;
    130 }
    131 
    132 /* Settings for buttons. */
    133 
    134 td.button
    135 {
    136   background: #E0E0E0;
    137   border: 1px outset #FFFFFF;
    138   font-weight: bold;
    139 }
    140