html {
  font-family:"Dejavu serif condensed", serif; font-size:11pt;
  text-align: justify;
  padding: 0;
  margin: 0;
  background-color: #eeeeec;
  color: #555753;
}

body {
  margin: 0;
  padding: 0;
}

#body-content {
  margin: 0 auto;
  padding: 1ex 2ex;
  max-width: 115ex;
}

#content {
  margin-left: 25ex;
}

pre {
  font-family:"Dejavu Sans Mono", fixed;
  background-color: #f5f5f5;
  -moz-border-radius: 1ex;
  padding: 1ex 1.5ex;
  font-size: 80%;
}
a {
  color: #4e9a06;
}
a:hover, a:focus {
  color: #f57900;
}
a:visited {
}
a:visited:hover {
}
hr {
  border-width: 0;
  height: 1px;
  background-color: #d3d7cf;
  margin: 0;
}
.linenumbers {
  float: left;
  margin-right: 1ex;
  text-align: right;
}
.linenumbers a, .linenumbers a:visited {
  text-decoration: none;
  color: #ccc;
}
h1, h2 {
  font-family: "Dejavu Sans", sans-serif;
  font-size: 120%;
  color: #f57900;
}
h2 {
  font-size: 110%;
  color: #555753;
}
.doc_browse {
  text-align: center;
}
.doc_browse .prev {
  float: left;
}
.doc_browse .next {
  float: right;
}

.centered {
  text-align: center;
}

img {
  vertical-align: middle;
  border: 0;
}

.abstract {
  font-style: italic;
}

#header {
  background: url(/images/header_background.png) repeat-x;
}
#header-logo {
  background: url(/images/header_logo.png) no-repeat;
}
#header-quote {
  background: url(/images/header_quote.png) no-repeat top right;
  height: 100px;
}
#header-content {
  padding: 20px 40px;
  color: #eeeeec;
  font-size: 250%;
  font-family: "Dejavu Sans", sans-serif;
}


#menu {
  float: left;
  width: 24ex;
  -moz-border-radius: 1ex;
  background-color: #e5e6e2;
  margin-top: 1ex;
}

#menu-content {
  padding: 1ex 0 1ex 1ex;
  color: #888;
  font-family: "Dejavu Sans", sans-serif;
}
#menu-content a {
  color: #888;
  text-decoration: none;
}
#menu-content a:hover {
  color: #555753;
}
#menu-content ul {
  margin: 0;
  padding: 0 0 0 1ex;
  list-style: none;
}
#menu-content li a {
  display:block;
}
#menu-content li a:before {
  content: "» ";
}
/*
TODO: Highlight selected item
#menu-content li a.selected {
  border-right: 5px solid #555753;
}
*/

dt {
  font-weight: bold;
}
blockquote {
  font-style: italic;
}
blockquote p:before {
  content: '«';
}
blockquote p:after {
  content: '»';
}
blockquote em {
  font-style: normal;
}

.dates {
  font-size: 80%;
  color: #aaa;
  border-top: 1px solid #d3d7cf;
}

acronym {
  cursor: help;
}