body {
  color: black;
  background: white;

  font-family: Arial, Helvetica, sans-serif;
/*
 * It's a Bad Idea(tm) to use fixed font sizes.
 * Uncomment it if you _really_ want
 */
  font-size: 14px;
}

div.table table, div.informaltable table {
  background: #333366;
  border-collapse: separate;
  border: solid 1px #333366;
  border-spacing: 1px;
}

div.table th, div.informaltable th {
  color: white;
  background: #4488cc;
  border: 0px;
  padding: 2px;
}

div.table td, div.informaltable td {
  background: #fffff8;
  border: 0px;
  padding: 2px;
}


pre.screen {
  padding: 4px;
  background: #e0e0e0;
}

pre.programlisting {
  padding: 4px;
  background: #e0e8f0;
}

/*
span.application {
}
*/

span.keycap {
  background: #ddd;
  border: solid 1px #aaa;
  white-space: nowrap;
  font-family: Arial, Helvetica, sans-serif;
}

span.guimenu, span.guisubmenu, span.guimenuitem {
  background: #dddddd;
}

tt.filename {
  color: maroon;
  white-space: nowrap;
}

tt.option {
  color: #066;
  white-space: nowrap;
}

div.example {
  padding-left: 0.5em;
  border-left: solid 2px black;
}

div.important .title, div.caution .title, div.warning .title {
  color: #c00;
}
/*
div.important, div.warning, div.caution {
  padding-left: 0.5em;
  border-left: solid 2px maroon;
}
*/