| author | haftmann | 
| Thu, 11 Mar 2021 07:05:29 +0000 | |
| changeset 73410 | 7b59d2945e54 | 
| parent 72962 | af2d0e07493b | 
| child 74679 | 0efa6a8b6e20 | 
| 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; }
 |