body {
    color: black;
    background-color: white;
    font: Verdana, Lucida, sans-serif;
    padding: 0;
    margin: 0;
    margin-left: 200px;
}

h1#title {
    float: right;
    color: white;
    background-color: black;
    font-size: 150px;
    padding: 0;
    margin: 0;
}

h1#title.wide {
    font-size: 100px;
}

h1#title.verywide {
    font-size: 75px;
}

div#logo {
    position: fixed;
    text-align: center;
    top: 0px;
    left: 0px;
    height: 200px;
    width: 190px;
}

div#logo h1 {
    font-size: 75px;
    padding: 0;
    margin: -10px 0;
}

div#logo p {
    padding: 0;
    margin: 5px 0;
    font-size:66%;
    font-style:italic;
}

div#linkbar {
    position: fixed;
    background-color: black;
    width: 190px;
    margin-right: 5px;
    left: 0px;
    top: 200px;
    bottom: 0px;
}

div#linkbar a {
    display: block;
    text-align: left;
    padding-top: 4px;
    color: white;
    text-decoration: none;
}

div#linkbar a:hover {
    text-decoration: underline;
}

div#linkbar .indent {
    display: block;
    margin-left: 25px;
}

.bgcompat {
    /* class for elements that should only appear
       on non-CSS-conforming UAs */
    display: none;
}

div#main {
    display: table;
    margin: 0 1em 0 0;
    padding: 0;
    clear: right;
}

div#main a {
    text-decoration: none;
    color: white;
    background-color: black;
    font-weight: bold;
}

div#contents a,
div#main a.toc-backref {
    background-color: white;
    color: black;
    font-weight: normal;
}

div#main a:hover {
    text-decoration: underline;
    color: black;
    background-color: white;
}

pre.listing {
    display: block;
    border: 1px solid black;
    margin: 0;
}

pre.listing:before {
    content: "code listing\A";
    display: block;
    color: white;
    background-color: black;
    padding: 5px;
    text-align: center;
}

div#footer {
    clear: both;
    text-align: right;
    font-style: italic;
    border-top: 1px solid black;
    margin-top: 4em;
}