body {font-family: Georgia, serif;
      line-height: 1.3;
      padding-left: 5em; padding-right: 1em;
      padding-bottom: 1em; max-width: 60em;}
table {border-collapse: collapse}
span.roman { font-family: century schoolbook, serif; font-weight: normal; }
h1, h2, h3, h4, h5, h6 {font-family:  Helvetica, sans-serif}
h4 { margin-top: 2.5em; }
dfn {font-family: inherit; font-variant: italic; font-weight: bolder }
kbd {font-family: monospace; text-decoration: underline}
/*var {font-family: Helvetica, sans-serif; font-variant: slanted}*/
var {font-variant: slanted;}
td  {padding-right: 1em; padding-left: 1em}
sub {font-size: smaller}
.node {padding: 0; margin: 0}

pre.lisp { font-family: monospace;
           background-color: #F4F4F4; border: 1px solid #AAA;
           padding-top: 0.5em; padding-bottom: 0.5em; }

/* coloring */

.lisp-bg { background-color: #F4F4F4 ; color: black; }
.lisp-bg:hover { background-color: #F4F4F4 ; color: black; }

.symbol { font-weight: bold; color: #770055; background-color : transparent; border: 0px; margin: 0px;}
a.symbol:link { font-weight: bold; color : #229955; background-color : transparent; text-decoration: none; border: 0px; margin: 0px; }
a.symbol:active { font-weight: bold; color : #229955; background-color : transparent; text-decoration: none; border: 0px; margin: 0px; }
a.symbol:visited { font-weight: bold; color : #229955; background-color : transparent; text-decoration: none; border: 0px; margin: 0px; }
a.symbol:hover { font-weight: bold; color : #229955; background-color : transparent; text-decoration: none; border: 0px; margin: 0px; }
.special { font-weight: bold; color: #FF5000; background-color: inherit; }
.keyword { font-weight: bold; color: #770000; background-color: inherit; }
.comment { font-weight: normal; color: #007777; background-color: inherit; }
.string  { font-weight: bold; color: #777777; background-color: inherit; }
.character   { font-weight: bold; color: #0055AA; background-color: inherit; }
.syntaxerror { font-weight: bold; color: #FF0000; background-color: inherit; }
span.paren1 { font-weight: bold; color: #777777; }
span.paren1:hover { color: #777777; background-color: #BAFFFF; }
span.paren2 { color: #777777; }
span.paren2:hover { color: #777777; background-color: #FFCACA; }
span.paren3 { color: #777777; }
span.paren3:hover { color: #777777; background-color: #FFFFBA; }
span.paren4 { color: #777777; }
span.paren4:hover { color: #777777; background-color: #CACAFF; }
span.paren5 { color: #777777; }
span.paren5:hover { color: #777777; background-color: #CAFFCA; }
span.paren6 { color: #777777; }
span.paren6:hover { color: #777777; background-color: #FFBAFF; }