/*
 * General stuff
 */

img {
    border: 0;
}

.textmode {
    display: none;
}

/*
 * A folio
 */

#page {
    margin: 0 auto;
    padding: 2em;
    max-width: 66ex;
    background-color: #FEFFF1;
    color: #000000;
    border: 2px solid #EEEFE1;
}

#page h1, #page h2, #page h3, #page h4 {
    font-family: sans-serif;
}

/*
 * The body
 */

@media print {
    #page #body {
        font-family: serif;
        line-height: 100%;
    }
}

#page #body p {
    padding: 0;
    margin: 0;
    /* Don't use as long as browser don't know how to break words...
     * text-align: justify;
     */
    font-family: sans-serif;
    line-height: 130%;
}

#page #body p + p {
    margin-top: 0.5em;
    /* This looks bad for some reason :-(
     * text-indent: 1em;
     */
}

#page #body blockquote {
    font-size: small;
    background-color: #EEEFE1;
    padding: 1em;
    border: 1px solid #DEDFD1;
}

#page #body div.acknowledgments {
    font-size: small;
    background-color: #EEEFE1;
    padding: 1em;
    margin: 1em;
    border: 1px solid #DEDFD1;
}

#page #body strong.acknowledgmentsheader {
    font-family: sans-serif;
}

#page #body pre {
    border-top: medium solid black;
    border-bottom: medium solid black;
    padding: 0.5em 0;
    margin-left: 2em;
    margin-right: 2em;
}

#page #body a {
    text-decoration: none;
    color: #006F00;
    border-bottom: 1px dotted black;
}

#page #body a.imglink {
    border-bottom: 0;
}

#page #body a:visited {
    border-bottom: 0;
}

#page #body .floatright {
    float: right;
    margin: 0 0 0.2em 0.5em;
}

#page #body .floatleft {
    float: left;
    margin: 0 0.5em 0.2em;
}

#page #body h1, #page #body h2, #page #body h3 {
    clear: both;
}

#page #body .sc {
    /* Small-caps is usually only emulated :-(
    font-variant: small-caps; */
    text-transform: uppercase;
}

#page #body .lang {
    vertical-align: middle;
    font-size: xx-small;
    color: #66666;
}

/*
 * The header line
 */

#page #header {
    font-family: sans-serif;
    font-size: small;
    min-height: 1.3em;
    border-bottom: 1px solid black;
}

#page #header #title {
    float: right;
    text-align: left;
}

#page #header #section {
    float: left;
    text-align: right;
}

#page #header a {
    text-decoration: none;
    color: black;
}

/*
 * The footer
 */

#page #footer {
    border-top: 1px solid black;
    margin-top: 1em;
    clear: both;
}

#page #footer {
    text-align: right;
    font-size: xx-small;
    min-height: 31px;
}

#page #footer #license {
    text-align: left;
    float: left;
    margin-top: 0.5em;
}

/*
 * Table of contents
 */

#page #toc ol {
    font-family: sans-serif;
    list-style-position: inside;
}

#page #toc ol.frontmatter, #page ol.backmatter {
    list-style: none;
}

#page #toc ol.frontmatter {
    margin-bottom: 0;
}

#page #toc ol.mainmatter {
    margin-top: 0;
    margin-bottom: 0;
}

#page #toc ol.backmatter {
    margin-top: 0;
}

/*
 * TeX, LaTeX and LaTeX 2e
 */

.tex-e {
  position: relative;
  top: 0.15em;
  left: -0.2em;
  margin-right: -0.35em;
  text-transform: uppercase;
  /* IE bogosity */
  _top: 0;
  _left: 0;
  _margin-right: 0;
  _text-transform: lowercase;
}

.latex-a {
  position: relative;
  font-size: 90%;
  top: -0.2em;
  left: -0.25em;
  margin-right: -0.35em;
  text-transform: uppercase;
  /* IE bogosity */
  _font-size: 100%;
  _top: 0;
  _left: 0;
  _margin-right: 0;
  _text-transform: lowercase;
}

.latex-epsilon {
  position: relative;
  top: 0.15em;
  /* IE bogosity */
  _top: 0;
}

/*
 * The weblog stuff
 */

#page #body h3.article {
    margin-bottom: 0;
}

#page #body div.articledate {
    font-size: small;
    font-style: italic;
    margin-bottom: 1em;
}

#page #footer #rss {
    text-align: left;
    float: left;
    margin: 0.5em 1em 0em 1em;
}

/*
 * htmlize styles
 */

.paren {
    color: #BEBFB1;
}

.comment {
    /* font-lock-comment-face */
    color: #ff0000;
}

.comment-delimiter {
    /* font-lock-comment-delimiter-face */
    color: #ff0000;
}

.doc {
    /* font-lock-doc-face */
    color: #00cf00;
}

.function-name {
    /* font-lock-function-name-face */
    color: #afaf00;
}

.keyword {
    /* font-lock-keyword-face */
    color: #00cfcf;
    font-weight: bold;
}

.string {
    /* font-lock-string-face */
    color: #00cf00;
}

.warning {
    /* font-lock-warning-face */
    color: #ff0000;
}