html {
  font-family: "Lucida Sans Unicode", "Lucida Grande", "Helvetica", "Sans-Serif";
  font-size: 14px;
}

* {
  box-sizing: border-box;
}

body {
  padding: 2em;
  margin: 0;
  width: 100%;
}

nav {
  position: absolute;
  top: 1em;
  right: 10em;
}

nav a {
  display: inline-block;
  padding: 0 0.5em;
}

div, section {
  padding: 0;
  margin: 0;
}

.subtext {
  padding: 0;
  margin-top: -1em;
  color: #bbb;
  font-size: 11px;
}

h1, h2 {
  font-weight: bold;
  margin: 0;
  margin-bottom: 0.5em;
  padding: 0;
}

h1 {
  font-size: 28px;
}

h2 {
  font-size: 22px;
}

section {
  padding: 1em 0;
  margin-bottom: 1em;
  display: block;
  width: 90%;
}

table {
  border: 1px solid #eee;
  border-collapse: collapse;
  width: 100%;
  table-layout: fixed;
}

td, th {
  border: 1px solid #eee;
  border-collapse: collapse;
  text-align: left;
  padding: 0.5em;
  word-wrap: break-word;
  vertical-align: top;
}

td p {
  padding: 0;
  margin: 0;
}

p.help {
  margin-top: 0.25em;
  color: #aaa;
}

td.index {
  text-align: right;
}

td.name {
  font-family: Monospace;
  color: #333;
}

.def {
  overflow: auto;
  font-family: Monospace;
  color: #333;
}

.malformed {
  color: #c00;
}