doc/geiser.css

   1 html {
   2     padding:0px;margin:0px;
   3     background-color:white;
   4     color:black;
   5     font-family:sans-serif;
   6     line-height:160%
   7 }
   8
   9 body {
  10     padding:10px 10% 10px 10%;
  11     margin:0px;
  12     text-align:justify;
  13     /* width: 750px; */
  14 }
  15
  16 a { color:black; weight=normal }
  17
  18 hr { height:0; color:white }
  19
  20 h2 {
  21     font-size:120%;
  22     text-transform:uppercase
  23 }
  24
  25 h3 {
  26     font-size:100%;
  27     text-transform:uppercase
  28 }
  29
  30 pre.code {
  31     display:block;
  32     padding:0px;
  33     margin-bottom:0px
  34 }
  35
  36 code {
  37     background-color:rgb(250, 250, 250);
  38     border:1px solid rgb(200, 200, 200);
  39     padding-left:4px;
  40     padding-right:4px
  41 }
  42
  43 pre.example {
  44     background-color:rgb(250, 250, 250);
  45     border:1px solid rgb(200, 200, 200);
  46     padding-left:4px;
  47     padding-right:4px;
  48 }
  49
  50 table { width: 100%; }
  51
  52 img {
  53     display:block;
  54     margin:10px auto 10px auto;
  55     border:none
  56 }
  57
  58 img.floatleft {
  59     float: left;
  60     margin: 4px;
  61     padding-right: 1em;
  62 }
  63
  64 img.floatright {
  65     float: right;
  66     margin: 4px;
  67     padding-left: 1em;
  68 }
  69
  70 ul {
  71     list-style-type:square;
  72     padding-left:1em;
  73     margin-left:1em
  74 }
  75
  76 kbd {
  77     font-weight: bold;
  78 }
  79
  80 div.navigation {
  81     background-color: #efebe7;
  82     line-height: 100%;
  83     top-margin: 5px;
  84     padding: 3px;
  85     /* background-color: #000000; */
  86     /* border-top-style: solid; */
  87     /* border-bottom-style: solid; */
  88     /* border-width: 0px; */
  89     /* border-top-width: 4px; */
  90     /* border-color: rgb(200, 200, 200); */
  91 }
  92
  93 .navlink {
  94     text-decoration: none;
  95     /* color: white; */
  96 }
  97
  98 .index-cp {
  99     line-height:120%;
 100     font-size: smaller;
 101 }