/* Literate programming + CWEB */
HTML {
  font-family: "Book Antiqua", "Century Schoolbook L", "Garamond", "DejaVu Serif", "Comic Sans MS", "URW Bookman L", "Latin Modern Math", "TeXGyrePagella", "Purisa", serif; 
/*
  "Georgia" is bad because "0" is like "o"
  "Bookman Old Style" not good: overlaps letters like "<var>g</var>" and "+")
*/
  font-size: 20px;
  text-align: left;
  background-color: white;
  color: #000000; 
}
BODY {
   margin-left: 8%;
   margin-right: 8%;
   font-size: 1em;
}
blockquote { 
  margin-left: 2em;
  margin-right: 2em;
}
blockquote.external { 
  margin-left: 2em;
  margin-right: 2em;
}
a:link {
  text-decoration: underline;
  text-decoration: none;
} 
a:visited {
  color: blue;
  text-decoration: none;
}
a:hover { /* Must come after :link and :visited */
  color: red;
  text-decoration: underline;
}
a:active {
  color: red;
  text-decoration: underline;
} 
h1 {
  hyphens: none;
  margin-top: 2em;
  margin-bottom: 2em;
}
h2 {
  hyphens: none;
  margin-top: 2em;
  margin-bottom: 1em;
}
.center {
  text-align: center;
}
.right {
}
p.epigraph {
  margin-top: 1.5em;
  margin-bottom: 1.5em;
  margin-left: 12%;
  hyphens: none;
  text-align: right;
  word-spacing: 0px;
  letter-spacing: 0px;
  font-size: 0.80em; /*0.80 x 20px = 16px*/
}
p.menu {
  text-align: right;
  font-size: 0.80em;
}
p.right {
  text-align: right;
}
p.big {
  font-size: 1.15em;;
}
.nw {
  white-space: nowrap;
  hyphens: none;
}
.small {
   font-size: 0.85em;
}
span.smallcaps {
/*font-style: italic;*/
  font-variant: small-caps;
}
small { /* DEPRECATE*/
  font-size: 87%;
}

p.gray { /* visible comments */
   color: #8080c0;
}
span.blood {
   color: #c00000; /*blood*/
}
span.gray { /* visible comments */
   color: #8080c0;
}
div.gray { /* visible comments */
   color: #8080c0;
}

span.hide { 
   /*color: #00d000;*/
   color: black;
   background-color: #d0ffd0;
}
p.hide { 
   /*color: #00d000;*/
   color: black;
   background-color: #d0ffd0;
}
div.hide { 
   /*color: #00d000;*/
   color: black;
   background-color: #d0ffd0;
}
li.hide { 
   /*color: #00d000;*/
   color: black;
   background-color: #d0ffd0;
}

span.tex { /*the "E" in "TEX"*/
  vertical-align: -0.15em;
  font-size: 90%;
}
span.latex { /*the "A" in "LaTEX"*/
  vertical-align: +0.3em;
  font-size: 70%;
}
kbd {
/*font-family: monospace, "Lucida Console", "Courier", "Monaco", "Menlo";*/
  font-family: "Menlo";
  font-family: "Monaco";
  font-family: "Courier"; /* Android does not have this :-( */
  font-family: "Lucida Console";
  font-family: monospace, monospace;
  font-size: 0.80em; /*=16px*/ 
}
pre {
/*font-family: monospace, "Lucida Console", "Courier", "Monaco", "Menlo";*/
  font-family: "Menlo";
  font-family: "Monaco";
  font-family: "Courier"; /* Android does not have this :-( */
  font-family: "Lucida Console";
  font-family: monospace;
  font-size: 0.80em; /*16px*/ 
  line-height: 130%;
}
table.box { 
  margin-top: 0em;
  margin-bottom: 0em;
  margin-left: auto;
  margin-right: auto;
  width: 90%;
  border: 0px solid black; /*scaffold*/   
}
div.boxx { 
  margin-top: 2em;
  margin-bottom: 2em;
  margin-left: auto;
  margin-right: auto;
  width: 90%;
  padding: 0.7em 0.7em 0.2em 0.7em;
  background-color: #ffffc0;
  font-size: 0.95em;
  border: 0px solid black; /*scaffold*/   
}
table.symbols { 
/* does not work in Chrome mobile...
  margin-left: auto;
  margin-right: auto;
*/
  margin-left: 4em;
  margin-top: 1em;
  margin-bottom: 1em;
  border-spacing: 0em 0em;
  border-collapse: collapse;
  font-size: 0.90em;
  border: 0px solid black; /*scaffold*/   
}
table.symbols td.a { 
  padding: 0.0em 1em 0.0em 0.3em;
  text-align: center;
  border: 0px solid black; /*scaffold*/   
  border-bottom: 0px solid #808080;
}
table.symbols td.b { 
  padding: 0.0em 0em 0.0em 0.3em;
  text-align: center;
  border: 0px solid black; /*scaffold*/   
  border-bottom: 0px solid #808080;
}
table.symbols td.c { 
  padding: 0.0em 0em 0.0em 2.5em;
  text-align: left;
  border: 0px solid black; /*scaffold*/   
  border-bottom: 0px solid #808080;
}
ul.bib { 
}
ul.bib li { 
  margin-top: 0.5em;
}
ul.bib p { 
  margin-top: 0.5em;
}
div.footer {
  hyphens: none;
  margin-top: 2em; 
  margin-bottom: 20em;
  word-spacing: 0px;
  letter-spacing: 0px;
  font-size: 0.85em; /*same as small*/
  line-height: normal; /*this is the default*/
}
div.footer p {
  margin-top: 0em;
  margin-bottom: 0em;
}
abbr {
   color: #000000;
   /* text-decoration: underline; */
}
abbr:hover {
   color: red;
   text-decoration: underline;
}
img.book {
  float: right;
  margin: 0em 1em 2em 1.5em;
}