author | wenzelm |
Wed, 06 Sep 2023 16:03:22 +0200 | |
changeset 78649 | d46006355819 |
parent 74679 | 0efa6a8b6e20 |
child 81566 | f207acb03ccb |
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; |
|
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
67336
diff
changeset
|
20 |
font-family: "Isabelle DejaVu Sans Mono", monospace; |
61374 | 21 |
} |
14542 | 22 |
|
72962 | 23 |
.contents { background-color: #FFFFFF; padding: 10px; } |
59120 | 24 |
.sessions { background-color: #FFFFFF; padding: 10px; } |
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
67336
diff
changeset
|
25 |
.document { white-space: normal; font-family: "Isabelle DejaVu Serif", serif; } |
14542 | 26 |
|
27848 | 27 |
.name { font-style: italic; } |
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
67336
diff
changeset
|
28 |
.filename { font-family: "Isabelle DejaVu Sans Mono", monospace; } |
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); } |
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
66076
diff
changeset
|
34 |
.control { font-weight: bold; font-style: italic; } |
33985 | 35 |
|
43550
b416425c7ad0
tuned color, to avoid confusion with type variables;
wenzelm
parents:
43549
diff
changeset
|
36 |
.binding { color: #336655; } |
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
37 |
.tfree { color: #A020F0; } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
38 |
.tvar { color: #A020F0; } |
66044 | 39 |
.free { color: #0000FF; } |
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
40 |
.skolem { color: #D2691E; } |
66044 | 41 |
.bound { color: #008000; } |
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
42 |
.var { color: #00009B; } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
43 |
.numeral { } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
44 |
.literal { font-weight: bold; } |
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
45 |
.delimiter { } |
66044 | 46 |
.inner_numeral { color: #FF0000; } |
47 |
.inner_quoted { color: #FF00CC; } |
|
55033 | 48 |
.inner_cartouche { color: #CC6600; } |
69351 | 49 |
.comment1 { color: #CC0000; } |
50 |
.comment2 { color: #FF8400; } |
|
51 |
.comment3 { color: #6600CC; } |
|
66044 | 52 |
.dynamic { color: #7BA428; } |
53 |
.class_parameter_color { color: #D2691E; } |
|
29320 | 54 |
|
43549
bb4cff2ff556
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm
parents:
43548
diff
changeset
|
55 |
.bold { font-weight: bold; } |
29320 | 56 |
|
66044 | 57 |
.main { color: #000000; } |
58 |
.command { font-weight: bold; } |
|
59 |
.keyword { font-weight: bold; } |
|
60 |
.keyword1 { color: #006699; } |
|
61 |
.keyword2 { color: #009966; } |
|
62 |
.keyword3 { color: #0099FF; } |
|
63 |
.quasi_keyword { color: #9966FF; } |
|
64 |
.operator { color: #323232; } |
|
59120 | 65 |
.string { color: #FF00CC; } |
66 |
.alt_string { color: #CC00CC; } |
|
67 |
.verbatim { color: #6600CC; } |
|
55033 | 68 |
.cartouche { color: #CC6600; } |
59120 | 69 |
.comment { color: #CC0000; } |
59125 | 70 |
.improper { color: #FF5050; } |
69972 | 71 |
.antiquote { color: #6600CC; } |
72 |
.raw_text { color: #6600CC; } |
|
73 |
.plain_text { color: #CC6600; } |
|
48751 | 74 |
.bad { background-color: #FF6A6A; } |
66075 | 75 |
.quoted { background-color: rgba(139,139,139,0.05); } |
76 |
.antiquoted { background-color: rgba(255,200,50,0.1); } |
|
65891 | 77 |
|
78 |
||
79 |
/* message background */ |
|
80 |
||
81 |
.writeln_message { background-color: #F0F0F0; } |
|
82 |
.information_message { background-color: #DCEAF3; } |
|
83 |
.tracing_message { background-color: #F0F8FF; } |
|
84 |
.warning_message { background-color: #EEE8AA; } |
|
85 |
.legacy_message { background-color: #EEE8AA; } |
|
86 |
.error_message { background-color: #FFC1C1; } |
|
65939 | 87 |
|
88 |
||
89 |
/* message underline */ |
|
90 |
||
91 |
.writeln { border-bottom: 1px dotted #C0C0C0; } |
|
92 |
.information { border-bottom: 1px dotted #C1DFEE; } |
|
93 |
.warning { border-bottom: 1px dotted #FF8C00; } |
|
94 |
.legacy { border-bottom: 1px dotted #FF8C00; } |
|
95 |
.error { border-bottom: 1px dotted #B22222; } |
|
96 |
||
97 |
||
98 |
/* tooltips */ |
|
99 |
||
100 |
.writeln { position: relative; display: inline-block; } |
|
101 |
.information { position: relative; display: inline-block; } |
|
102 |
.warning { position: relative; display: inline-block; } |
|
103 |
.legacy { position: relative; display: inline-block; } |
|
104 |
.error { position: relative; display: inline-block; } |
|
105 |
||
106 |
.writeln:hover .tooltip { visibility: visible; } |
|
107 |
.information:hover .tooltip { visibility: visible; } |
|
108 |
.warning:hover .tooltip { visibility: visible; } |
|
109 |
.legacy:hover .tooltip { visibility: visible; } |
|
110 |
.error:hover .tooltip { visibility: visible; } |
|
111 |
||
112 |
.tooltip { |
|
65947 | 113 |
top: -0.5ex; |
114 |
left: 5em; |
|
65939 | 115 |
visibility: hidden; |
65982 | 116 |
width: 50em; |
65939 | 117 |
border: 1px solid #808080; |
65941 | 118 |
padding: 1px 1px; |
65939 | 119 |
background-color: #FFFFE9; |
120 |
position: absolute; |
|
121 |
z-index: 1; |
|
122 |
} |
|
65945 | 123 |
|
124 |
.tooltip pre { margin: 1px; white-space: pre-wrap; } |
|
74679 | 125 |
|
126 |
||
127 |
/* formal entities */ |
|
128 |
||
129 |
.entity_def { |
|
130 |
color: inherit; |
|
131 |
text-decoration: inherit; |
|
132 |
} |
|
133 |
||
134 |
.entity_def:hover { |
|
135 |
color: inherit; |
|
136 |
text-decoration: inherit; |
|
137 |
background-color: rgba(50,50,50,20%); |
|
138 |
} |
|
139 |
||
140 |
.entity_ref { |
|
141 |
color: inherit; |
|
142 |
text-decoration: inherit; |
|
143 |
border: 0.5px solid rgba(0,0,0,0); |
|
144 |
} |
|
145 |
||
146 |
.entity_ref:hover { |
|
147 |
color: inherit; |
|
148 |
text-decoration: inherit; |
|
149 |
background-color: rgba(50,50,50,20%); |
|
150 |
border: 0.5px solid black; |
|
151 |
} |