utility.css

   1 body {
   2         margin : 2em;
   3         padding : 0em;
   4         font-family : sans-serif;
   5         font-size : 12px;
   6 }
   7
   8 p.warning {
   9         color : red;
  10 }
  11
  12 p.query, code {
  13         color : green;
  14 }
  15
  16 p.insensitive {
  17         color : gray;
  18 }
  19
  20 .floatingLogo {
  21         float : right;
  22 }
  23
  24 a {
  25         color : #4684ff;
  26         text-decoration : none;
  27 }
  28
  29 a:hover {
  30         color : black;
  31 }
  32
  33 div.notice {
  34         background : #ffffff;
  35         border : 1px solid #88b0f0;
  36         width : 50%;
  37         padding : 5px;
  38         margin : 0px 0px 5px 0px;
  39         font-size : 9pt;
  40 }
  41
  42 div.warning {
  43         background : #fff7d5;
  44         border : 1px solid #d7c47a;
  45         font-size : 9pt;
  46         width : 50%;
  47         padding : 5px;
  48         margin : 0px 0px 5px 0px;
  49 }
  50
  51
  52 div.warning img, div.notice img, div.error img {
  53         vertical-align : middle;
  54         padding : 5px;
  55 }
  56
  57 div.error {
  58         border : 1px solid #ff0000;
  59         background : #ffcccc;
  60         padding : 5px;
  61         margin : 0px 0px 5px 0px;
  62         font-size : 9pt;
  63         width : 50%;
  64 }
  65
  66 h1 {
  67         color : #88b0f0;
  68         font-size : 16pt;
  69 /*      border-width : 0px 0px 1px 0px;
  70         border-color : black;
  71         border-style : solid; */
  72 }
  73
  74 h2 {
  75         color : #88b0f0;
  76         font-size : 14pt;
  77 /*      border-width : 0px 0px 1px 0px;
  78         border-color : black;
  79         border-style : solid; */
  80 }
  81
  82 div.rss h1 {
  83         border-width : 0px 0px 1px 0px;
  84         border-color : gray;
  85         border-style : dotted;
  86         color : gray;
  87         margin-right : 90px;
  88 }
  89
  90 div.rss h2 {
  91         font-size : 12pt;
  92         margin : 0px;
  93 }
  94
  95 div.rss a.extlink {
  96         color : gray;
  97         border-width : 0px 0px 1px 0px;
  98         border-color : #778899;
  99         border-style : dotted;
 100         font-size : 9pt;
 101 }
 102
 103 div.rss p.description {
 104         color : gray;
 105         font-size : 9pt;
 106 }
 107
 108 div.rss div.content {
 109         margin-top : 0.5em;
 110 }
 111
 112 div.rss img.feedicon {
 113         float : right;
 114 }
 115
 116 div.rss hr {
 117         border-width : 0px 0px 1px 0px;
 118         border-style : dashed;
 119         border-color : #e0e0e0;
 120 }
 121
 122