author | wenzelm |
Sat, 16 Dec 2017 16:46:01 +0100 | |
changeset 67215 | 03d0c958d65a |
parent 66076 | 8bd8750a2f9b |
child 67255 | f1f983484878 |
permissions | -rw-r--r-- |
65837 | 1 |
/* standard document markup */ |
2 |
||
3 |
dt { |
|
4 |
float: left; |
|
5 |
clear: left; |
|
6 |
padding-right: 0.5em; |
|
7 |
font-weight: bold; |
|
8 |
} |
|
9 |
||
66039
a2b8c3d31037
explicit foreground color, for the sake of dark theme in VSCode;
wenzelm
parents:
66000
diff
changeset
|
10 |
body { |
a2b8c3d31037
explicit foreground color, for the sake of dark theme in VSCode;
wenzelm
parents:
66000
diff
changeset
|
11 |
color: #000000; |
a2b8c3d31037
explicit foreground color, for the sake of dark theme in VSCode;
wenzelm
parents:
66000
diff
changeset
|
12 |
background-color: #FFFFFF; |
a2b8c3d31037
explicit foreground color, for the sake of dark theme in VSCode;
wenzelm
parents:
66000
diff
changeset
|
13 |
} |
14542 | 14 |
|
15 |
.head { background-color: #FFFFFF; } |
|
61374 | 16 |
.source { |
62812
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
61374
diff
changeset
|
17 |
direction: ltr; unicode-bidi: bidi-override; |
61374 | 18 |
background-color: #FFFFFF; |
19 |
padding: 10px; |
|
20 |
font-family: IsabelleText; |
|
66076
8bd8750a2f9b
avoid overlapping line background, notably for "quoted";
wenzelm
parents:
66075
diff
changeset
|
21 |
line-height: 147%; |
61374 | 22 |
} |
14542 | 23 |
|
59120 | 24 |
.theories { background-color: #FFFFFF; padding: 10px; } |
25 |
.sessions { background-color: #FFFFFF; padding: 10px; } |
|
14542 | 26 |
|
27848 | 27 |
.name { font-style: italic; } |
28 |
.filename { font-family: fixed; } |
|
23716 | 29 |
|
27848 | 30 |
|
33985 | 31 |
/* basic syntax markup */ |
27848 | 32 |
|
63683
87c6158f4ef4
more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
wenzelm
parents:
62813
diff
changeset
|
33 |
.hidden { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); } |
33985 | 34 |
|
43550
b416425c7ad0
tuned color, to avoid confusion with type variables;
wenzelm
parents:
43549
diff
changeset
|
35 |
.binding { color: #336655; } |
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
36 |
.tfree { color: #A020F0; } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
37 |
.tvar { color: #A020F0; } |
66044 | 38 |
.free { color: #0000FF; } |
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
39 |
.skolem { color: #D2691E; } |
66044 | 40 |
.bound { color: #008000; } |
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
41 |
.var { color: #00009B; } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
42 |
.numeral { } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
43 |
.literal { font-weight: bold; } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
44 |
.delimiter { } |
66044 | 45 |
.inner_numeral { color: #FF0000; } |
46 |
.inner_quoted { color: #FF00CC; } |
|
55033 | 47 |
.inner_cartouche { color: #CC6600; } |
59120 | 48 |
.inner_comment { color: #CC0000; } |
66044 | 49 |
.dynamic { color: #7BA428; } |
50 |
.class_parameter_color { color: #D2691E; } |
|
29320 | 51 |
|
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
52 |
.bold { font-weight: bold; } |
29320 | 53 |
|
66044 | 54 |
.main { color: #000000; } |
55 |
.command { font-weight: bold; } |
|
56 |
.keyword { font-weight: bold; } |
|
57 |
.keyword1 { color: #006699; } |
|
58 |
.keyword2 { color: #009966; } |
|
59 |
.keyword3 { color: #0099FF; } |
|
60 |
.quasi_keyword { color: #9966FF; } |
|
61 |
.operator { color: #323232; } |
|
59120 | 62 |
.string { color: #FF00CC; } |
63 |
.alt_string { color: #CC00CC; } |
|
64 |
.verbatim { color: #6600CC; } |
|
55033 | 65 |
.cartouche { color: #CC6600; } |
59120 | 66 |
.comment { color: #CC0000; } |
59125 | 67 |
.improper { color: #FF5050; } |
48751 | 68 |
.bad { background-color: #FF6A6A; } |
66075 | 69 |
.quoted { background-color: rgba(139,139,139,0.05); } |
70 |
.antiquoted { background-color: rgba(255,200,50,0.1); } |
|
65891 | 71 |
|
72 |
||
73 |
/* message background */ |
|
74 |
||
75 |
.writeln_message { background-color: #F0F0F0; } |
|
76 |
.information_message { background-color: #DCEAF3; } |
|
77 |
.tracing_message { background-color: #F0F8FF; } |
|
78 |
.warning_message { background-color: #EEE8AA; } |
|
79 |
.legacy_message { background-color: #EEE8AA; } |
|
80 |
.error_message { background-color: #FFC1C1; } |
|
65939 | 81 |
|
82 |
||
83 |
/* message underline */ |
|
84 |
||
85 |
.writeln { border-bottom: 1px dotted #C0C0C0; } |
|
86 |
.information { border-bottom: 1px dotted #C1DFEE; } |
|
87 |
.warning { border-bottom: 1px dotted #FF8C00; } |
|
88 |
.legacy { border-bottom: 1px dotted #FF8C00; } |
|
89 |
.error { border-bottom: 1px dotted #B22222; } |
|
90 |
||
91 |
||
92 |
/* tooltips */ |
|
93 |
||
94 |
.writeln { position: relative; display: inline-block; } |
|
95 |
.information { position: relative; display: inline-block; } |
|
96 |
.warning { position: relative; display: inline-block; } |
|
97 |
.legacy { position: relative; display: inline-block; } |
|
98 |
.error { position: relative; display: inline-block; } |
|
99 |
||
100 |
.writeln:hover .tooltip { visibility: visible; } |
|
101 |
.information:hover .tooltip { visibility: visible; } |
|
102 |
.warning:hover .tooltip { visibility: visible; } |
|
103 |
.legacy:hover .tooltip { visibility: visible; } |
|
104 |
.error:hover .tooltip { visibility: visible; } |
|
105 |
||
106 |
.tooltip { |
|
65947 | 107 |
top: -0.5ex; |
108 |
left: 5em; |
|
65939 | 109 |
visibility: hidden; |
65982 | 110 |
width: 50em; |
65939 | 111 |
border: 1px solid #808080; |
65941 | 112 |
padding: 1px 1px; |
65939 | 113 |
background-color: #FFFFE9; |
114 |
position: absolute; |
|
115 |
z-index: 1; |
|
116 |
} |
|
65945 | 117 |
|
118 |
.tooltip pre { margin: 1px; white-space: pre-wrap; } |