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