body {background: white;
      color:      black;
      margin:     10px
     }
h1   {text-align: center;
      color:      black;
      font-size: 140%
     }

h2   {font-size: 120%}

.term {color: blue;
       font-style: italic}

.java {color: #0000A0}

.emph {color: #0000B0}

.subst {color: red;
        font-style: italic}

.warn {color: #800080}

.bar  {background-color: #FFFFE0
      }

.direction {background-color: #FFFFE0;
            font-size: 100%}

table.normal {font-size: 100%}