/* Originally cribbed from http://bluerobot.com/web/layouts/layout1.html
 * However, people who merge the hotlink colors are evil and should be killed,
 * so I removed that.  Fixing font sizes in pixels is evil, too; is much as
 * possible I have moved all dimensions to be relative to the associated font
 * size. Finally, light grey is a great background color, but lousy for
 * foreground text on white.
 *
 * The only size in here that's tied to something external is the pixel size
 * for the menu width.  This is sized to just fit a Google "wide skyscraper"
 * ad, which is 160x600.
 */

body {
  margin: 0;
  padding: 0;
  font-family: helvetica, sans-serif;
  color: #333;
  background-image: url(paper.gif);
}

p {
  font-family: helvetica, sans-serif;
  margin: 0 0 1em 0;
  padding: 0;
}

#Content > p {
  text-indent: 2em;
  margin: 0;
}

#Content > p + p {
  text-indent: 2em;
  margin-top: 1ex;
}

h1 {
  font-size: x-large;
  margin-bottom: 0.25ex;
}

h2 {
  font-size: large;
  margin-bottom: 0.25ex;
}

a {
  text-decoration: none;
  font-family: verdana, arial, helvetica, sans-serif;
}

a:hover {
  background-color: #ccc;
}

#Header {
  font-weight: 600;
  font-size: x-large;	/* should be same as an h1 header */
  margin: 20px 0 10px 0;
  padding: 0 0 2ex 20px;
  border-style: solid;
  border-color: black;
  border-width: 1px 0;
  background-color: #eee;
  height: 1ex;
}

#Content {
  /* Left margin is menu width + 40 pixels */
  margin: 0 50px 50px 200px;
  padding: 10px;
}


#Menu {
  float:left;
  top: 80px;
  left: 20px;
  width: 160px;
  padding: 0.5em;
  margin: 0.5em;
  background-color: #eee;
  border: 1px dashed #999;
}

/* For internal tables of contents on a page. E.g. hacking.html. */
ol.ToC {
  list-style: upper-roman;
}

div.strike {
  text-decoration: line-through;
}

@media print {
  #Content {
    /* Left margin is menu width + 3em */
    margin: 0 50px 50px 0;
    padding: 10px;
  }

  #Menu {
    display: none;
  }
}

/* For convenience */
.centered {
  text-align: center;
  margin-left: auto;
  margin-right: auto;
}

.right {
  float: right;
  margin: 0;
}

.notebox {
  background-color: #eee;
  border: 1px dashed #999;
  margin: 15px;
  font-size: small;
  text-indent: 0;
}