1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
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; }
|
