/*
  Good style ideas stolen from Debathena.
  Hey, we use some different fonts.
  And the colors are unmistakably different.
*/

/* Basic fonts and sizes. */
html {
    font-size: 87.5%;
}
body {
    font-family: Tahoma, Sans, sans-serif;
}
pre, code, samp, kbd, tt {
    font-family: "Bitstream Vera Sans Mono", "Luxi Mono", "Courier New", monospace;
    font-size: 100%;
}

/* Blue headings. */
h1, h2, h3, h4, h5, h6 {
    color: #13a;
}

/* Dividing line under the header. */
h1 {
    border-bottom: 1px solid black;
    margin-top: 0;
    overflow: auto;
}

pre {
    background: #f6f6f6;
    border: 1px solid #ddd;
    padding: .125em;
}
a:link, a:visited {
    text-decoration: none;
}
a:link:hover, a:visited:hover {
    text-decoration: underline;
}

/* Keep help-popup links unbolded in e.g. table headings. */
.helplink {
  font-weight: normal;
}

/* Highlight error messages in bright red. */
.error {
  color: #FF0000;
  padding: 0.25em;
}
td.error {
  border: 1px solid red;
}

/* Navigation bar. */
.navigation {
  padding: 0em 1em;
  font-size: 125%;
  font-weight: bold;
  font-family: "Trebuchet MS", Trebuchet, Sans, sans-serif;
}
.navigation li {
  display: inline;
  padding: .2em;
}

/* Logged-in welcome message. */
.loggedin {
  float: right;
}
.loggedin .name {
  font-weight: bold;
}