doc/atdoc/index.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   text-decoration: none;
  10   color: black;
  11   border-bottom: 1px solid #9c0000;
  12 }
  13
  14 .nonlink {
  15   border-bottom: 1px solid white;
  16   border-top: 1px solid white;
  17   border-left: 1px solid white;
  18   border-right: 1px solid white;
  19   padding-top: 1px;
  20   padding-bottom: 1px;
  21 }
  22
  23 .sidebar a {
  24   border-top: 1px solid #eeeeee;
  25   border-left: 1px solid #eeeeee;
  26   border-right: 1px solid #eeeeee;
  27 }
  28
  29 #headerlink {
  30   border: none;
  31 }
  32
  33 #headerlink:hover {
  34   border: none;
  35 }
  36
  37 body {
  38   color: #000000;
  39   background-color: #ffffff;
  40   margin-top: 2em;
  41   margin-right: 20pt;
  42   margin-bottom: 10%;
  43   font-family: verdana, arial;
  44 }
  45
  46 .main {
  47   margin-top: 20px;
  48   margin-left: 40px;
  49 }
  50
  51 .padded {
  52   padding-left: 30px;
  53 }
  54
  55 .padded h1,h2 {
  56   margin-left: -30px;
  57 }
  58
  59 h2 {
  60   color: #9c0000;
  61 }
  62
  63 .page-title {
  64   color: black;
  65 }
  66
  67 h3 {
  68   color: #9c0000;
  69   width: 90%;
  70   border-bottom: 1px solid #9c0000;
  71    margin-left: -3px;
  72    padding-left: 3px;
  73 }
  74
  75 h4 {
  76 }
  77
  78 .grau {
  79   padding-top: 1em;
  80 }
  81
  82 pre {
  83   background-color: #eeeeee;
  84   border: solid 1px #d0d0d0;
  85   padding: 1em;
  86   margin-right: 10%;
  87 }
  88
  89 .code {
  90   border: solid 1px #d0d0d0;
  91   padding: 1em;
  92   margin-right: 10%;
  93 }
  94
  95 .indent {
  96   margin-left: 20px;
  97   padding-bottom: 1em;
  98 }
  99
 100 .def {
 101   padding: 1px 1px 1px 1px;
 102   margin-bottom: 1px;
 103   font-weight: bold;
 104   margin-right: 40px;
 105 }
 106
 107 .nomargin {
 108   margin-bottom: 0;
 109   margin-top: 0;
 110 }
 111
 112 .noindent {
 113   margin-left: -30px;
 114   padding-bottom: 1em;
 115 }
 116
 117 #header {
 118   margin-right: 22px;
 119   border-bottom: 1px solid black;
 120   font-family: verdana, arial;
 121   font-size: 12pt;
 122   padding-bottom: 1px;
 123 }