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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
code, .code {
font-size: 9pt;
font-family: Courier, Courier New, monospace;
color:#007000;
}
kbd {
font-family: Courier, Courier New, monospace;
font-weight: bold;
}
pre.ebnf {
background-color: beige;
}
pre.grammar {
background-color: beige;
}
p.rule {
font-style: italic
}
span.event {
font-style: italic
}
body {
font: 13px Helvetica, Arial, sans-serif;
}
h1, h2, h3, h4, h5, h6 {
font-family: Helvetica, Arial, sans-serif;
margin-bottom: 0.25em;
}
h2 {
background-color: #e5ecf9;
margin-top: 2em;
border-top:1px solid #36C;
}
pre{
font-size: 9pt;
background-color: #fafaff;
margin: 1em 0 0 0;
padding: .99em;
line-height: 125%;
overflow: auto;
word-wrap: break-word;
}
li {
padding-bottom: 0.5em;
}
li pre {
margin: 0.5em 0px 1em 0px;
}
/* Above this comment, styles meant to help page authors achieve beauty. */
/* Below this comment, styles used in the boilerplate-ish parts of pages. */
div#content {
margin-left: 20%;
padding: 0 1em 2em 1em;
margin-top: -2px;
border: 2px solid #e5ecf9;
}
#topnav {
margin: 0px;
padding: .1em 0px;
width: 100%;
white-space: nowrap;
background-color: #e5ecf9;
border-top:1px solid #36C;
font: bold large Helvetica, Arial, sans-serif;
}
div#linkList {
font: 13px Helvetica, Arial, sans-serif;
float: left;
width: 20%;
}
div#linkList ul {
padding: 1px;
list-style-type: none;
}
div#linkList li {
margin-left: 1em;
}
div#linkList li.navhead {
font-weight: bold;
margin-left: 0px;
}
#nav dl {
margin: 0 0.5em 0 0.5em;
padding: 0px;
}
.navtop {
font-size: xx-small;
float: right;
}
#footer {
margin: 2em;
text-align: center;
color: #555;
font-size: small;
}
#footer a {
color: #555;
}
@media print {
div#linkList {
display: none;
}
.navtop {
display: none;
}
div#content {
margin-left: 0px;
border: none;
}
}
|
