1@charset "iso-8859-1";
2
3/* Global settings. */
4
5body
6{
7  background: #FFFFFF;
8}
9
10h1
11{
12  text-align: center;
13}
14
15h2
16{
17  background: #EEEEFF;
18  padding: 10px;
19}
20
21dt
22{
23  padding: 6px;
24}
25
26dt div 
27{
28  color: grey;
29  float: right;
30}
31
32dd
33{
34  padding: 6px;
35}
36
37pre
38{
39  padding: 10px;
40  background: #E0E0E0;
41}
42
43.spacious li
44{
45  padding: 8px;
46}
47
48.shifted li
49{
50  margin-left: 50px;
51}
52
53img.float
54{
55  float: left;
56}
57
58a
59{
60  text-decoration: none;
61}
62
63a.button
64{
65  color: #000000;
66  text-decoration: none;
67  background: #E0E0E0;
68  border: 1px outset #FFFFFF;
69  float: right;
70}
71
72/* Settings for variable width code. */
73
74p.code
75{
76  padding: 10px;
77  background: #E0E0E0;
78}
79
80
81/* Settings for diagrams. */
82
83table.diagram
84{
85  padding: 8px;
86  border: none;
87  border-spacing: 2px;
88}
89
90td.transparentblock
91{
92  text-align: center;
93  padding: 10px 0px;
94}
95
96td.whiteblock
97{
98  width: 100px;
99  text-align: center;
100  border: 1px solid #C0C0C0;
101  background: #E0E0E0;
102  padding: 10px 0px;
103}
104
105td.lightblock
106{
107  width: 100px;
108  text-align: center;
109  border: 1px solid #8888FF;
110  background: #BBBBFF;
111  padding: 20px 0px;
112}
113
114td.darkblock
115{
116  width: 100px;
117  text-align: center;
118  background: #8888FF;
119  padding: 20px 0px;
120}
121
122/* Settings for buttons. */
123
124td.button
125{
126  background: #E0E0E0;
127  border: 1px outset #FFFFFF;
128  font-weight: bold;
129}
130