doc/index.css

   1 a {
   2   text-decoration: none;
   3   color: black;
   4   border-bottom: 1px solid #0070a0 /* default color */;
   5 }
   6
   7 .colored {
   8   color: #0070a0 /* default color */;
   9 }
  10
  11 a:hover {
  12   color: #0070a0 /* default color */;
  13   border-bottom: 1px solid #aaaaaa;
  14 }
  15
  16 body {
  17   color: #000000;
  18   background-color: #ffffff;
  19   margin-top: 2em;
  20   margin-right: 0pt;
  21   margin-bottom: 10%;
  22   font-family: verdana, arial;
  23 }
  24
  25 .main {
  26   margin-top: 20px;
  27   margin-left: 40px;
  28   padding-left: 30px;
  29 }
  30
  31 h1,h2,h3 {
  32   color: #0070a0 /* default color */;
  33   margin-top: 2em;
  34   margin-left: -30px;
  35 }
  36
  37 .def {
  38   border-bottom: 1px solid black;
  39   padding: 1px 1px 1px 1px;
  40   margin-bottom: 1px;
  41   font-weight: bold;
  42   margin-right: 40px;
  43 }
  44
  45 .def:hover {
  46   background-color: #0070a0 /* default color */;
  47 }
  48
  49 .def a {
  50   text-decoration: none;
  51   color: #000000;
  52   border-bottom: 0px solid white;
  53   border-top: 0px solid white;
  54   border-left: 0px solid white;
  55   border-right: 0px solid white;
  56 }
  57
  58 .def a:hover {
  59   background-color: #0070a0 /* default color */;
  60   color: #000000;
  61   text-decoration: none;
  62   border-bottom: 0px solid white;
  63   border-top: 0px solid white;
  64   border-left: 0px solid white;
  65   border-right: 0px solid white;
  66 }
  67
  68 .nomargin {
  69   margin-bottom: 0;
  70   margin-top: 0;
  71 }
  72
  73 .noindent {
  74   margin-left: -30px;
  75 }
  76
  77 #header {
  78   padding-bottom: 1px;
  79   width: 70%;
  80   border-bottom: 1px solid black;
  81   font-family: verdana, arial;
  82   font-size: 15pt;
  83 }
  84
  85 .code {
  86   background-color: #eeeeee;
  87   border: solid 1px #d0d0d0;
  88   padding: 1em;
  89   width: 60%;
  90 }
  91
  92 .example {
  93   background-color: #eeeeee;
  94   border: solid 1px #d0d0d0;
  95   padding: 1em;
  96   margin-bottom: 0;
  97   width: 60%;
  98 }
  99
 100 .result {
 101   border: solid 1px #d0d0d0;
 102   border-top: 0px;
 103   padding: 1em;
 104   margin-top: 0;
 105   width: 60%;
 106 }
 107
 108 div.sidebar {
 109   float: right;
 110   min-width: 30%;
 111   padding: 0pt 5pt 5pt 5pt;
 112   font-family: verdana, arial;
 113 }
 114
 115 div.sidebar-title {
 116   font-weight: bold;
 117   background-color: #0070a0 /* default color */;
 118   border: solid #0070a0 /* default color */;
 119   border-top-width: 1px;
 120   border-bottom-width: 2px;
 121   border-left-width: 4px;
 122   border-right-width: 0px;
 123   padding-left: 1px;
 124   margin: 0em 2pt 0px 2em;
 125 }
 126
 127 div.sidebar-title a {
 128   color: #ffffff;
 129 }
 130
 131 div.sidebar-main {
 132   background-color: #f7f7f7;
 133   border: solid #0070a0 /* default color */;
 134   border-top-width: 0px;
 135   border-bottom-width: 0px;
 136   border-left-width: 4px;
 137   border-right-width: 0px;
 138   margin: 0em 2pt 1em 2em;
 139   padding: 1em;
 140 }
 141
 142 div.sidebar ul.main {
 143   padding: 0pt 0pt 0pt 1em;
 144   margin: 0 0 1em;
 145 }
 146
 147 div.sidebar ul.sub {
 148   list-style-type: square;
 149   padding: 0pt 0pt 0pt 1em;
 150   margin: 0 0 1em;
 151 }
 152
 153 div.sidebar ul.hack {
 154   padding: 0 0 0 0;
 155   margin: 0 0 1em;
 156   list-style-type: none;
 157 }