utility.css

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