body {
  font-size:   Small;
  line-height: 130%;
}

pre {
  line-height: 100%;
}

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

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

.small {
  font-size:    75%;
}

.javacode {
  font-size:    75%;
  padding:    0.5em;
  background: #ffcccc;
  border:     2px solid #990000;
}

.smalljavacode {
  font-size:    50%;
  padding:    0.5em;
  background: #ffcccc;
  border:     2px solid #990000;
}

.cli {
  font-size:    75%;
  padding:    0.5em;
  background: #000000;
  color:      #ffffff;
  border:     4px solid #808080
}

.smallcli {
  font-size:    50%;
  padding:    0.5em;
  background: #000000;
  color:      #ffffff;
  border:     4px solid #808080
}

.output {
  font-size:    75%;
  padding:    0.5em;
  background: #ccccff;
  border:     2px solid #000099
}

.smalloutput {
  font-size:    50%;
  padding:    0.5em;
  background: #ccccff;
  border:     2px solid #000099
}

a { text-decoration: none; }

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

h1 {
  text-align: center;
}

a:link {
  color:         #404040;
}

a:visited {
  color:         #404040;
}

a:hover {
  color:         #ff2020;
}

.page {
  border: 1px solid white;
  font-size:      20pt;
  padding: 0;
  padding-left:   20px;
  padding-right:  20px;
  line-height:    130%;
  width:          750px;
  height:         520px;
  background:     #ffffff;
  font-family:    Helvetica;
}

.header {
  height:     25px;
  border-bottom:  2px solid #990000;
  background: #ff9999;
  color:      #990000;
}

.footer {
  height:     15px;
  background: #ffffff;
}

.header,.footer {
  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:    180%;
  font-family:  Arial,Helvetica;
  font-weight:  bold;
  text-align:   left;
}

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