body {
 // font-family: sans-serif;
 font-family:  Charter, Georgia, Bookman, Times New Roman, Times, serif;
 color: white;
 background-color: #000000; 
 background-image: url(x-black.png);
 background-repeat: no-repeat;
 background-position: 0 0;
 background-attachment: fixed;
}

body a:link {
  color: #9999FF;
  text-decoration: none;
}
body a:visited {
  color: #9999FF;
  text-decoration: none;
}
body a:hover {
  color: #9999FF;
  text-decoration: underline;
}

div.funnyfont {
  font-family:  Georgia, Bookman, Times New Roman, Times, serif;
}

.running-text {
  width: 70ex;
}

.wider-running-text {
}

code {
  font-family:  Courier New, Courier, monospace;
  font-size: 120%
  white-space: nowrap; /* pre would be better, but it doesn't work with IE */
}

.codedisplay {
  font-family:  Courier New, Courier, monospace;
  margin: 10px;
  padding: 20px;
  border-width: 20px;
  text-style: center;
  white-space: pre;
  color: white;
  border-color: FFFF00;
  border-width: thin;
  border-style: solid;
  background-color: 000066;
  background-image: url(x-blue.png);
  background-repeat: no-repeat;
  background-position: 0 0; 
  background-attachment: fixed;
}

.figure {
  margin: 10px;
  padding: 20px;
  border-width: 20px;
  text-style: center;
  color: white;
  border-color: FFFF00;
  border-width: thin;
  border-style: solid;
  background-color: 000066;
  background-image: url(x-blue.png);
  background-repeat: no-repeat;
  background-position: 0 0; 
  background-attachment: fixed;
}

.title {
  font-family: sans-serif;
  font-size: 250%;
  text-align: right;
}

.robby {
  text-align: right;
}

.bordertop {
  border-top: thin solid #FFFFFF;
}

.navbar-spacer {
  color: green;
  white-space: pre;
  text-align: right;
  font-weight: bold;
  background-color: transparent;
  opacity: 0.0;
  filter: alpha(opacity=0);
  width: 100%;
}

/* navbar (used for top navbar and section tocs) */
.navbar {
  color: black;
  background-color: transparent;
  text-decoration: none;
  font-weight: bold;
  white-space: pre;
  text-align: right;
  position: fixed;
}

.navbar a:link {
  color: AAAAFF;
  background-color: transparent;
  text-decoration: none;
  font-weight: bold;
}
.navbar a:visited {
  color: AAAAFF;
  background-color: transparent;
  text-decoration: none;
  font-weight: bold;
}
.navbar a:active {
  color: AAAAFF;
  text-decoration: underline;
  font-weight: bold;
}
.navbar a:hover {
  color: AAAAFF;
  text-decoration: underline;
  font-weight: bold;
}

/* current link */
.disabled {
  color: #606060;
}