tutorial/tutorial.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 }
  12
  13 .nonlink {
  14   border-bottom: 1px solid white;
  15   border-top: 1px solid white;
  16   border-left: 1px solid white;
  17   border-right: 1px solid white;
  18   padding-top: 1px;
  19   padding-bottom: 1px;
  20 }
  21
  22 #headerlink {
  23   border: none;
  24 }
  25
  26 #headerlink:hover {
  27   border: none;
  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 .navigation {
  40   position: absolute;
  41   right: 10%;
  42   bottom: 10%;
  43   font-family: verdana, arial;
  44   font-size: 24pt;
  45 }
  46
  47 .icon {
  48   padding-left: 10px;
  49   padding-right: 10px;
  50   color: #55a6e0;
  51 }
  52
  53 .em {
  54   color: #407da9;
  55 }
  56
  57 .blue {
  58   color: #55a6e0;
  59 }
  60
  61 .spacy li {
  62    padding-bottom: 1em;
  63 }
  64
  65 .spacy ul {
  66    padding-top: 1em;
  67 }
  68
  69 .main {
  70   padding-left: 10%;
  71   padding-right: 10%;
  72   margin-top: 20px;
  73   margin-left: 40px;
  74   font-family: verdana, arial;
  75   font-size: 14pt;
  76 }
  77
  78 .main h1 {
  79   margin-top: 1em;
  80   margin-bottom: 1em;
  81   color: #55a6e0;
  82 }
  83
  84 .padded {
  85   padding-left: 30px;
  86 }
  87
  88 .padded h1,h2 {
  89   margin-left: -30px;
  90 }
  91
  92 h2 {
  93   color: #0070a0;
  94 }
  95
  96 .page-title {
  97   color: black;
  98 }
  99
 100 h3 {
 101   color: #0070a0;
 102   width: 90%;
 103   border-bottom: 1px solid #0070a0;
 104    margin-left: -3px;
 105    padding-left: 3px;
 106 }
 107
 108 h4 {
 109 }
 110
 111 .grau {
 112   padding-top: 1em;
 113 }
 114
 115 pre {
 116   padding: 1em;
 117   margin-right: 10%;
 118 }
 119
 120 /*
 121 .code {
 122   border: 2px dotted #55a6e0;
 123   padding: 1em;
 124   font-size: 10pt;
 125 }
 126 */
 127
 128 /*
 129 .repl {
 130   border-top: 1px solid #cccccc;
 131   border-left: 1px solid #cccccc;
 132   border-right: 1px solid #cccccc;
 133   margin-bottom: 0;
 134   padding: 1em;
 135   font-size: 10pt;
 136 }
 137
 138 .result {
 139   border-top: 2px dotted #55a6e0;
 140   border-left: 2px dotted #55a6e0;
 141   border-right: 2px dotted #55a6e0;
 142   border-bottom: 2px dotted #55a6e0;
 143   margin-top: 0;
 144   padding: 1em;
 145   font-size: 10pt;
 146 }
 147 */
 148
 149 .code {
 150   border: 1px solid #aaaaaa;
 151   background-color:  #d0e8f8;
 152   margin-bottom: 0;
 153   padding: 1em;
 154   font-size: 10pt;
 155 }
 156
 157 .inline-code {
 158   margin-bottom: 0;
 159   padding: 3px;
 160   font-size: 10pt;
 161 }
 162
 163 .example-header {
 164   padding-top: 3px;
 165   padding-bottom: 3px;
 166   padding-left: 10px;
 167   margin-right: 10%;
 168   color: white;
 169   background-color: black;
 170   margin-top: 3em;
 171   margin-bottom: 0;
 172   font-weight: bold;
 173 }
 174
 175 .example .repl { margin-top: 0; }
 176 .example pre { margin-top: 0; }
 177 .example b { font-weight: normal; }
 178
 179 .repl {
 180   border-top: 1px solid #aaaaaa;
 181   border-left: 1px solid #aaaaaa;
 182   border-right: 1px solid #aaaaaa;
 183   margin-bottom: 0;
 184   padding: 1em;
 185   font-size: 10pt;
 186   background-color:  #d0e8f8;
 187 }
 188
 189 .result {
 190   border-left: 1px solid #aaaaaa;
 191   border-right: 1px solid #aaaaaa;
 192   border-bottom: 1px solid #aaaaaa;
 193   margin-top: 0;
 194   padding: 1em;
 195   font-size: 10pt;
 196 }
 197
 198 .indent {
 199   margin-left: 20px;
 200   padding-bottom: 1em;
 201 }
 202
 203 .def {
 204   padding: 1px 1px 1px 1px;
 205   margin-bottom: 1px;
 206   font-weight: bold;
 207   margin-right: 40px;
 208 }
 209
 210 .nomargin {
 211   margin-bottom: 0;
 212   margin-top: 0;
 213 }
 214
 215 .noindent {
 216   margin-left: -30px;
 217   padding-bottom: 1em;
 218 }
 219
 220 #header {
 221   margin-right: 22px;
 222   border-bottom: 1px solid black;
 223   font-family: verdana, arial;
 224   font-size: 12pt;
 225   padding-bottom: 1px;
 226 }