helm/software/lambda-delta/xml/ld-html.css

   1 @charset "UTF-8";
   2
   3 /* general ******************************************************************/
   4
   5 body {
   6    background: rgb(255, 255, 255);
   7    color: rgb(0, 0, 0);
   8    margin: 2.5%;
   9 }
  10
  11 a:link, a:visited {
  12    text-decoration: underline;
  13 }
  14
  15 a:active, a:hover, a:focus {
  16    background: rgb(192, 192, 192);
  17 }
  18
  19 /* blocks *******************************************************************/
  20
  21 .spacer {
  22    text-align: center;
  23 }
  24
  25 .head1 {
  26    margin: 0.5em 0;
  27    text-align: center;
  28    font-weight: bold;
  29    font-size: xx-large;
  30 }
  31
  32 .head2 {
  33    margin: 0.5em 0;
  34    text-align: left;
  35    font-weight: bold;
  36    font-size: x-large;
  37 }
  38
  39 .text {
  40    margin: 1em 0;
  41    text-align: left;
  42 }
  43
  44 /* inline decorations *******************************************************/
  45
  46 .icon32 {
  47    border: 0;
  48    width: 32px;
  49    height: 32px;
  50 }
  51
  52 .rule {
  53    border: 0;
  54    height: 4px;
  55    width: 100%;
  56 }
  57
  58 .w3c {
  59    margin: 0 0.5em;
  60    border: 0;
  61    width: 88px;
  62    height: 32px; /* this should be 31px */
  63 }
  64
  65 /* terms ********************************************************************/
  66
  67 .separator {
  68    background: rgb(255, 255, 255);
  69    color: rgb(0, 0, 0);
  70 }
  71
  72 .sort {
  73    background: rgb(255, 255, 255);
  74    color: rgb(128, 0, 255);
  75 }
  76
  77 .lref {
  78    background: rgb(255, 255, 255);
  79    color: rgb(0, 0, 0);
  80 }
  81
  82 .gref {
  83    background: rgb(255, 255, 255);
  84    color: rgb(0, 0, 255);
  85 }
  86
  87 .appl {
  88    background: rgb(255, 255, 255);
  89    color: rgb(0, 0, 0);
  90 }
  91
  92 .cast {
  93    background: rgb(255, 255, 255);
  94    color: rgb(255, 0, 0);
  95 }
  96
  97 .local {
  98    background: rgb(255, 255, 255);
  99    color: rgb(0, 160, 0);
 100 }
 101
 102 .global {
 103    background: rgb(255, 255, 255);
 104    color: rgb(0, 0, 0);
 105 }