doc/boxy.css

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