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 ul.spacious li
     38 {
     39   padding: 8px;
     40 }
     41 
     42 a
     43 {
     44   text-decoration: none;
     45 }
     46 
     47 a.button {
     48   color: #000000;
     49   text-decoration: none;
     50   background: #E0E0E0;
     51   border: 1px outset #FFFFFF;
     52   float: right;
     53 }
     54 
     55 /* Settings for variable width code. */
     56 
     57 p.code {
     58   padding: 10px;
     59   background: #E0E0E0;
     60 }
     61 
     62 
     63 /* Settings for diagrams. */
     64 
     65 table.diagram {
     66   padding: 8px;
     67   border: none;
     68   border-spacing: 2px;
     69 }
     70 
     71 td.transparentblock {
     72   text-align: center;
     73   padding: 10px 0px;
     74 }
     75 
     76 td.whiteblock {
     77   width: 100px;
     78   text-align: center;
     79   border: 1px solid #C0C0C0;
     80   background: #E0E0E0;
     81   padding: 10px 0px;
     82 }
     83 
     84 td.lightblock {
     85   width: 100px;
     86   text-align: center;
     87   border: 1px solid #8888FF;
     88   background: #BBBBFF;
     89   padding: 20px 0px;
     90 }
     91 
     92 td.darkblock {
     93   width: 100px;
     94   text-align: center;
     95   background: #8888FF;
     96   padding: 20px 0px;
     97 }
     98 
     99 /* Settings for buttons. */
    100 
    101 td.button {
    102   background: #E0E0E0;
    103   border: 1px outset #FFFFFF;
    104   font-weight: bold;
    105 }
    106