body {
	margin: 0px;
	padding: 0px;
    background-color: white;
    font-family: Helvetica, Arial, sans-serif;
	text-rendering: optimizeLegibility;
}

hr {
    height: 1px;
	border: none;
	color: black;
	background-color: black;
}

h2 {
	font-variant: small-caps;
	font-weight: bold;
	color:  #444444;
    margin-top: 1em;
	margin-bottom: 1em;
    font-size: 125%;
}

h3 {
	font-variant: small-caps;
	font-weight: bold;
	color:  #444444;
    margin-top: 1em;
	margin-bottom: 1em;
    font-size: 125%;
}

.banner {
	margin-bottom: 1em;
	text-align: center;
}

.bannercontent {
	padding: .5em;
	max-width: 65em;
	/* Need to center */
	margin-left: auto;
	margin-right: auto;
}

.bodytext {
/*	border: 1px solid red;*/
	line-height: 133%; /* From practicaltypography.com */
	text-align: center;  /* child elements need text-align: left; */
/*	overflow: hidden; */
	padding-left: 2em;
	padding-right: 2em;
}

.navbar {
	display: inline-block; /* so parent's text-align: center; centers us */
	text-align: left; /* undo text-align: center; from parent */
	vertical-align: top;
    max-width: 10em;
}

.content {
/*	border: 1px solid gray;*/
	display: inline-block; /* so parent's text-align: center; centers us */
	text-align: left; /* undo text-align: center; from parent */

	max-width: 45em; /* From practicaltypography.com */
/*	line-height: 133%; */
	/* Need to center body if we use a width */
/*	margin-left: auto;
	margin-right: auto; */
	/* Pad so that widths less than max-width have a margin */
/*	padding-left: 2em;
	padding-right: 2em; */
}

.content table {  /* <table> seems to ignore this >:( */
	line-height: 133%;
}

.footer {
	margin-top: 2em;
	text-align: center;
}

.heading {
	font-size: 150%;
	font-weight: bold;
}

/* ----- show/hide toggles ------ */
.showHideBlock a {
	color: unset;
	text-decoration: none;
}
.showHideBlock a:hover {
	text-decoration: underline;
}

/* --------- banner ------------- */
.title {
	font-weight: bold;
	font-size: 200%;
	line-height: 133%;  /* bug?  line-height doesn't scale with font-size */
}

.subtitle {
	font-size: 150%;
	line-height: 133%;  /* bug?  line-height doesn't scale with font-size */
}

.supertitle {
	font-weight: bold;
	font-size: 100%;
	line-height: 100%;
	text-align: left;
}

/* ---------- menu -------------- */
.menubar {
	border-top: 1px solid black;
	padding-top: .25em;
	text-align: right;
}

.menu {
	position: 
	padding-left: 2em;
	padding-right: 2em;
	font-weight: bold;
}

.menu a {
	display: inline-block;
	color: unset;
	text-decoration: none;
	width: 100%;
}

.menu a:hover {
	text-decoration: underline;
}

.menuframe {
	padding-top: .25em;
	padding-bottom: .25em;
	border: 1px solid rgb(128, 128, 128);
	background-color: rgba(255, 255, 255, .9);
	box-shadow: 0 .4em .4em .2em rgba(0, 0, 0, .25);
	font-weight: normal;
	white-space: nowrap;
}

.menu:hover .menuframe {
	visibility: visible;
}

.menuitem {
	margin: 0px;
	padding-top: 0px;
	padding-bottom: 0px;
	padding-left: .5em;
	padding-right: .5em;
	text-decoration: none;
	line-height: 133%;
}

.menuitem:hover {
	background-color: rgba(245, 245, 245, .9);
}

/* ---------- code -------------- */
pre { margin: 0; }  /* default stylesheet has margin: 1em */
.codeContainer { margin-left: 2em; margin-right: 2em;
                 line-height: 110%; }
.codeComment { color: #008800; }
.codeKeyword { color: #0033aa; }
.codeType { color: #116666; }
.codeConstant { color: #8800aa; }
.codeFunctionCall { font-weight: bold; color: #555555; }