/* basic font formatting stuff */

body { 
  font-family: sans-serif;
  background-color: White; 
  color: Black; 
	padding-left: 50px;
}

a { font-style: italic; }
a:link { color: #8080ff; }
a:visited { color: #6060b0; }
a:active { color: #000000; }

.news:first-line { font-weight: bold; }

.center { text-align: center;  }
.top    { vertical-align: top; }

pre.code {
  font-size: 120%;
  padding: 0.5% 1%;
  border: 1px dashed #6060B0;
  background-color: #A0A0FF;
  overflow: hidden;
}


/* centered text block for the start page */

div#startpage {
  text-align: center;
  margin-left: auto;
  margin-right: auto;
  width: 45em;
}


/* menu positioning and interactive stuff */

div.content {
	position: absolute;
	top:     0em;
	left: 17.5em;
}

div.menu {
	position: fixed;
	top:  0px;
	left: 0px;
}

object.menu {
	height: 100em;
}

ul.menu {
  cursor: pointer;
  font-weight: bold;
}

ul.menu ul {
  cursor: default;
  display: block;
  font-weight: normal;
  position: relative;
  left: -1.5em;
}