Home | History | Annotate | Download | only in manual 
      1 @charset "iso-8859-1";
      2 
      3 /* Global settings. */
      4 
      5 body {
      6   background: #FFFFFF;
      7 }
      8 
      9 h1 {
     10   text-align: center;
     11 }
     12 
     13 h2 {
     14   background: #EEEEFF;
     15   padding: 10px;
     16 }
     17 
     18 dt {
     19   padding: 6px;
     20 }
     21 
     22 dt div 
     23 {
     24   color: grey;
     25   float: right;
     26 }
     27 
     28 dd {
     29   padding: 6px;
     30 }
     31 
     32 pre {
     33   padding: 10px;
     34   background: #E0E0E0;
     35 }
     36 
     37 a
     38 {
     39   text-decoration: none;
     40 }
     41 
     42 /* Settings for variable width code. */
     43 
     44 p.code {
     45   padding: 10px;
     46   background: #E0E0E0;
     47 }
     48 
     49 
     50 /* Settings for diagrams. */
     51 
     52 table.diagram {
     53   padding: 8px;
     54   border: none;
     55   border-spacing: 2px;
     56 }
     57 
     58 td.transparentblock {
     59   text-align: center;
     60   padding: 10px 0px;
     61 }
     62 
     63 td.whiteblock {
     64   width: 100px;
     65   text-align: center;
     66   border: solid #C0C0C0 1px;
     67   background: #E0E0E0;
     68   padding: 10px 0px;
     69 }
     70 
     71 td.lightblock {
     72   width: 100px;
     73   text-align: center;
     74   border: solid #8888FF 1px;
     75   background: #BBBBFF;
     76   padding: 20px 0px;
     77 }
     78 
     79 td.darkblock {
     80   width: 100px;
     81   text-align: center;
     82   background: #8888FF;
     83   padding: 20px 0px;
     84 }
     85 
     86 /* Settings for buttons. */
     87 
     88 td.button {
     89   background: #E0E0E0;
     90   border: outset #FFFFFF 1px;
     91   font-weight: bold;
     92 }
     93