style.css revision b72c5c2e5482cf10117b2b25f642f7616b2326c3 
1@charset "iso-8859-1";
2
3/* Global settings. */
4
5body {
6  background: #FFFFFF;
7}
8
9h1 {
10  text-align: center;
11}
12
13h2 {
14  background: #EEEEFF;
15  padding: 10px;
16}
17
18dt {
19  padding: 6px;
20}
21
22dt div 
23{
24  color: grey;
25  float: right;
26}
27
28dd {
29  padding: 6px;
30}
31
32pre {
33  padding: 10px;
34  background: #E0E0E0;
35}
36
37a
38{
39  text-decoration: none;
40}
41
42/* Settings for variable width code. */
43
44p.code {
45  padding: 10px;
46  background: #E0E0E0;
47}
48
49
50/* Settings for diagrams. */
51
52table.diagram {
53  padding: 8px;
54  border: none;
55  border-spacing: 2px;
56}
57
58td.transparentblock {
59  text-align: center;
60  padding: 10px 0px;
61}
62
63td.whiteblock {
64  width: 100px;
65  text-align: center;
66  border: solid #C0C0C0 1px;
67  background: #E0E0E0;
68  padding: 10px 0px;
69}
70
71td.lightblock {
72  width: 100px;
73  text-align: center;
74  border: solid #8888FF 1px;
75  background: #BBBBFF;
76  padding: 20px 0px;
77}
78
79td.darkblock {
80  width: 100px;
81  text-align: center;
82  background: #8888FF;
83  padding: 20px 0px;
84}
85
86/* Settings for buttons. */
87
88td.button {
89  background: #E0E0E0;
90  border: outset #FFFFFF 1px;
91  font-weight: bold;
92}
93