body, td {
  font-size:   14px;
  line-height: 130%;
}

pre {
  font-size: 50%;
  line-height: 100%;
}

body {
  padding: 0;
  margin: 0;
  background:     #ffffff;
  width: 798px;
}

.hilite {
  text-decoration: underline;
}

.toc {
  font-size:    75%;
  line-height: 100%;
}

a { text-decoration: none; }

h1, h2, h3, h4, h5, h6 { 
  color:  #000099;
  line-height: 100%;
}

h1 {
  text-align: center;
}

a:link {
  color:         #0000ff;
}

a:visited {
  color:         #0000a0;
}

a:hover {
  color:         #2020ff;
}

.page {
  border: 1px dotted gray;
  font-size:      18pt;
  padding: 0;
  padding-left:   20px;
  padding-right:  20px;
  line-height:    130%;
  width:          756px;
  height:         534px;
  background:     #ffffff;
  font-family:    Helvetica;
}

.header {
  border-bottom:  2px solid #000099;
}

.footer {
  border-top:     2px solid #000099;
}

.header,.footer {
  background: #9999ff;
  height:     20px;
  width:      100%;
  margin:     0;
  padding-left:    15px;
  padding-right:   15px;
}

.header-links,.footer-links {
  text-align: right;
}

.header-links img {
  border: 0px; 
}

.header-text {
  font-size:    140%;
  font-family:  Arial,Helvetica;
  font-weight:  bold;
  text-align:   left;
}

.footer-text {
  text-align: right;
  font-style: italic;
}

.smallfont {
  font-size:    50%;
  line-height:  100%;
}

.smallfontright {
  font-size:    50%;
  line-height:  100%;
  float: right;
  vertical-align: top
}

.smallfontrightside {
  width:        25%;
  font-size:    50%;
  line-height:  100%;
  float: right;
  bottom: 100%;
  vertical-align: top
}

.javacode {
  font-size:    80%;
  padding:    0.5em;
  background: #ddddff;
  border:     2px solid #000077;
}

.smalljavacode {
  font-size:  12px;
  line-height: 130%;
  padding:    0.5em;
  background: #ddddff;
  border:     2px solid #000077;
}

.diff {
  color: 0000ff;
  background: #bbbbff;
}

.mark {
  border: 1px solid red;
}

.centered { 
  text-align: center;
}