/* $Id: style.css 359 2009-02-19 10:06:39Z zw $ */

body {
  background-color: rgb(204,221,255);
  color: rgb(0,0,0);
  font-family: sans-serif;
  font-weight: normal;
}

a { text-decoration: none }

a:link { color: rgb(153,0,51) }

a:visited { color: rgb(0,153,51) }

a:link:hover, a:active, a:active:hover, a:visited:hover
{
  color: rgb(255,0,0);  background-color:  rgb(204,204,204);
}

h1, h2, h3 {
  font-weight: bold;
  margin-top: 1.5em;
}

h2 { font-size: 100% }

h1 {
  font-size: 130%;
}

.linenum, .numwarn, .numerror, .numinfo {
  text-align: right;
  color: rgb(0,0,255);
}

.numwarn, .warn {
  color: rgb(0,128,0);
}

.numerror, .error {
  color: rgb(255,0,0);
}

.numinfo, .info {
  color: rgb(204,102,0);
}

.line, .warn, .error, .info { text-align: left }

.val { color: rgb(255,0,255) }