pintos-os.org Git - pintos-anon/blob - doc/pintos.css

   1 body {
   2         background: white;
   3         color: black;
   4         padding: 0em 12em 0em 3em;
   5         margin: 0
   6 }
   7 body>p {
   8         margin: 0pt 0pt 0pt 0em
   9 }
  10 body>p + p {
  11         margin: .75em 0pt 0pt 0pt
  12 }
  13 H1 {
  14         font-size: 150%;
  15         margin-left: -1.33em
  16 }
  17 H2 {
  18         font-size: 125%;
  19         font-weight: bold;
  20         margin-left: -.8em
  21 }
  22 H3 {
  23         font-size: 100%;
  24         font-weight: bold;
  25         margin-left: -.5em }
  26 H4 {
  27         font-size: 100%;
  28         margin-left: 0em
  29 }
  30 H1, H2, H3, H4, H5, H6 {
  31         font-family: sans-serif;
  32         color: blue
  33 }
  34 html {
  35         margin: 0
  36 }
  37 code {
  38         font-family: sans-serif
  39 }
  40
  41 a:link {
  42         color: blue;
  43         text-decoration: none;
  44 }
  45 a:visited {
  46         color: gray;
  47         text-decoration: none;
  48 }
  49 a:active {
  50         color: black;
  51         text-decoration: none;
  52 }
  53 a:hover {
  54         text-decoration: underline
  55 }
  56
  57 div.menu {
  58         margin: 0;
  59         font-size: 80%;
  60         font-weight: bold;
  61         line-height: 1.1;
  62         text-align: center;
  63         position: absolute;
  64         top: 2em;
  65         left: auto;
  66         width: 8.5em;
  67         right: 2em;
  68 }
  69 div.menu p, span.menuitem {
  70         display: block;
  71         margin: 0;
  72         padding: 0.3em 0.4em;
  73         font-family: Arial, sans-serif;
  74         background: #ddd;
  75         border: thin outset #000;
  76         color: #000;
  77         text-indent: 0em;
  78 }
  79 IMG.menuimg {
  80         width: 50%;
  81         height: auto;
  82         border-width: 0
  83 }
  84
  85 div.menu a, div.menu em {
  86         display: block;
  87         margin: 0 0.5em
  88 }
  89 div.menu a, div.menu em {
  90         border-top: 2px groove #000
  91 }
  92 div.menu a:first-child {
  93         border-top: none
  94 }
  95 div.menu em {
  96         color: #fff
  97 }
  98
  99 div.menu a:link {
 100         text-decoration: none;
 101         color: blue
 102 }
 103 div.menu a:visited {
 104         text-decoration: none;
 105         color: gray
 106 }
 107 div.menu a:hover {
 108         background: blue;
 109         color: white
 110 }
 111
 112 div.menu span.menugap + span.menuitem {
 113         display: block;
 114         margin-top: 1em
 115 }
 116
 117 span.hide {
 118         display: none
 119 }
 120
 121 body>div.menu {
 122         position: fixed
 123 }
 124
 125 address {
 126         font-size: 90%;
 127         font-style: normal
 128 }