doc/blue.css

   1 body {
   2   color: #000000;
   3   background-color: #ffffff;
   4   margin-top: 2em;
   5   margin-right: 20pt;
   6   margin-bottom: 10%;
   7   font-family: times, serif;
   8 }
   9
  10 a {
  11   color: #000077;
  12   border-bottom: 1px solid #ccccff;
  13 }
  14
  15 .main {
  16   margin-top: 20px;
  17   margin-left: 40px;
  18 }
  19
  20 .padded {
  21   padding-left: 30px;
  22 }
  23
  24 .padded h1,h2 {
  25   margin-left: -30px;
  26 }
  27
  28 .nonlink {
  29   border-bottom: 1px solid white;
  30   border-top: 1px solid white;
  31   border-left: 1px solid white;
  32   border-right: 1px solid white;
  33   padding-top: 1px;
  34   padding-bottom: 1px;
  35 }
  36
  37 h3 {
  38   width: 90%;
  39   color: #000000;
  40   border-bottom: 1px solid #7777cc;
  41   margin-left: -3px;
  42   padding-left: 3px;
  43 }
  44
  45 h4 {
  46 }
  47
  48 .grau {
  49   padding-top: 1em;
  50 }
  51
  52 .code {
  53   border: solid 1px #d0d0d0;
  54   padding: 1em;
  55   margin-right: 10%;
  56 }
  57
  58 .indent {
  59   margin-left: 20px;
  60   padding-bottom: 1em;
  61 }
  62
  63 .def {
  64   padding: 1px 1px 1px 1px;
  65   margin-bottom: 1px;
  66   font-weight: bold;
  67   margin-right: 40px;
  68 }
  69
  70 .nomargin {
  71   margin-bottom: 0;
  72   margin-top: 0;
  73 }
  74
  75 .noindent {
  76   margin-left: -30px;
  77   padding-bottom: 1em;
  78 }
  79
  80 #header {
  81   margin-right: 22px;
  82   border-bottom: 1px solid #7777cc;
  83   font-family: times, serif;
  84   font-size: 12pt;
  85   padding-bottom: 1px;
  86 }
  87
  88 #headerlink {
  89   border: none;
  90 }
  91
  92 #headerlink:hover {
  93   border: none;
  94 }