| author | wenzelm |
| Fri, 27 Dec 2024 16:54:48 +0100 | |
| changeset 81667 | c03e21a4cc26 |
| parent 69354 | 600727ff6889 |
| permissions | -rw-r--r-- |
|
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:
diff
changeset
|
1 |
SplineFontDB: 3.0 |
|
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:
diff
changeset
|
2 |
FontName: Vacuous |
|
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:
diff
changeset
|
3 |
FullName: Vacuous |
|
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:
diff
changeset
|
4 |
FamilyName: Vacuous |
|
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:
diff
changeset
|
5 |
Weight: Medium |
|
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:
diff
changeset
|
6 |
Copyright: |
|
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:
diff
changeset
|
7 |
UComments: "2016-8-12: Created." |
|
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:
diff
changeset
|
8 |
Version: 001.000 |
|
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:
diff
changeset
|
9 |
ItalicAngle: 0 |
|
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:
diff
changeset
|
10 |
UnderlinePosition: -100 |
|
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:
diff
changeset
|
11 |
UnderlineWidth: 50 |
|
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:
diff
changeset
|
12 |
Ascent: 800 |
|
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:
diff
changeset
|
13 |
Descent: 200 |
|
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:
diff
changeset
|
14 |
LayerCount: 2 |
|
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:
diff
changeset
|
15 |
Layer: 0 0 "Back" 1 |
|
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:
diff
changeset
|
16 |
Layer: 1 0 "Fore" 0 |
|
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:
diff
changeset
|
17 |
XUID: [1021 906 1711068302 5949507] |
|
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:
diff
changeset
|
18 |
FSType: 8 |
|
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:
diff
changeset
|
19 |
OS2Version: 0 |
|
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:
diff
changeset
|
20 |
OS2_WeightWidthSlopeOnly: 0 |
|
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:
diff
changeset
|
21 |
OS2_UseTypoMetrics: 1 |
|
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:
diff
changeset
|
22 |
CreationTime: 1471028867 |
|
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
23 |
ModificationTime: 1513953645 |
|
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:
diff
changeset
|
24 |
PfmFamily: 17 |
|
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:
diff
changeset
|
25 |
TTFWeight: 500 |
|
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:
diff
changeset
|
26 |
TTFWidth: 5 |
|
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:
diff
changeset
|
27 |
LineGap: 90 |
|
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:
diff
changeset
|
28 |
VLineGap: 0 |
|
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:
diff
changeset
|
29 |
OS2TypoAscent: 0 |
|
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:
diff
changeset
|
30 |
OS2TypoAOffset: 1 |
|
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:
diff
changeset
|
31 |
OS2TypoDescent: 0 |
|
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:
diff
changeset
|
32 |
OS2TypoDOffset: 1 |
|
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:
diff
changeset
|
33 |
OS2TypoLinegap: 90 |
|
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:
diff
changeset
|
34 |
OS2WinAscent: 0 |
|
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:
diff
changeset
|
35 |
OS2WinAOffset: 1 |
|
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:
diff
changeset
|
36 |
OS2WinDescent: 0 |
|
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:
diff
changeset
|
37 |
OS2WinDOffset: 1 |
|
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:
diff
changeset
|
38 |
HheadAscent: 0 |
|
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:
diff
changeset
|
39 |
HheadAOffset: 1 |
|
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:
diff
changeset
|
40 |
HheadDescent: 0 |
|
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:
diff
changeset
|
41 |
HheadDOffset: 1 |
|
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:
diff
changeset
|
42 |
OS2Vendor: 'PfEd' |
|
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:
diff
changeset
|
43 |
MarkAttachClasses: 1 |
|
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:
diff
changeset
|
44 |
DEI: 91125 |
|
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:
diff
changeset
|
45 |
LangName: 1033 |
|
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:
diff
changeset
|
46 |
Encoding: UnicodeFull |
|
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:
diff
changeset
|
47 |
UnicodeInterp: none |
|
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:
diff
changeset
|
48 |
NameList: Adobe Glyph List |
|
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:
diff
changeset
|
49 |
DisplaySize: -96 |
|
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:
diff
changeset
|
50 |
AntiAlias: 1 |
|
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:
diff
changeset
|
51 |
FitToEm: 1 |
|
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
52 |
WinInfo: 0 20 14 |
|
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:
diff
changeset
|
53 |
BeginPrivate: 0 |
|
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:
diff
changeset
|
54 |
EndPrivate |
|
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:
diff
changeset
|
55 |
TeXData: 1 0 0 346030 173015 115343 0 1048576 115343 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144 |
|
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
56 |
BeginChars: 1114112 11 |
|
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:
diff
changeset
|
57 |
|
|
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:
diff
changeset
|
58 |
StartChar: uni2759 |
|
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:
diff
changeset
|
59 |
Encoding: 10073 10073 0 |
|
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:
diff
changeset
|
60 |
Width: 44 |
|
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:
diff
changeset
|
61 |
VWidth: 1670 |
|
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:
diff
changeset
|
62 |
Flags: HW |
|
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:
diff
changeset
|
63 |
LayerCount: 2 |
|
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:
diff
changeset
|
64 |
Fore |
|
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:
diff
changeset
|
65 |
SplineSet |
|
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:
diff
changeset
|
66 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
67 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
68 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
69 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
70 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
71 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
72 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
73 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
74 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
75 |
EndSplineSet |
|
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:
diff
changeset
|
76 |
EndChar |
|
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:
diff
changeset
|
77 |
|
|
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:
diff
changeset
|
78 |
StartChar: uni21E9 |
|
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:
diff
changeset
|
79 |
Encoding: 8681 8681 1 |
|
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:
diff
changeset
|
80 |
Width: 44 |
|
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:
diff
changeset
|
81 |
VWidth: 1670 |
|
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:
diff
changeset
|
82 |
Flags: HW |
|
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:
diff
changeset
|
83 |
LayerCount: 2 |
|
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:
diff
changeset
|
84 |
Fore |
|
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:
diff
changeset
|
85 |
SplineSet |
|
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:
diff
changeset
|
86 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
87 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
88 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
89 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
90 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
91 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
92 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
93 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
94 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
95 |
EndSplineSet |
|
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:
diff
changeset
|
96 |
EndChar |
|
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:
diff
changeset
|
97 |
|
|
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:
diff
changeset
|
98 |
StartChar: uni21E7 |
|
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:
diff
changeset
|
99 |
Encoding: 8679 8679 2 |
|
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:
diff
changeset
|
100 |
Width: 44 |
|
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:
diff
changeset
|
101 |
VWidth: 1670 |
|
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:
diff
changeset
|
102 |
Flags: HW |
|
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:
diff
changeset
|
103 |
LayerCount: 2 |
|
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:
diff
changeset
|
104 |
Fore |
|
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:
diff
changeset
|
105 |
SplineSet |
|
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:
diff
changeset
|
106 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
107 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
108 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
109 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
110 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
111 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
112 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
113 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
114 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
115 |
EndSplineSet |
|
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:
diff
changeset
|
116 |
EndChar |
|
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:
diff
changeset
|
117 |
|
|
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:
diff
changeset
|
118 |
StartChar: uni21D6 |
|
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:
diff
changeset
|
119 |
Encoding: 8662 8662 3 |
|
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:
diff
changeset
|
120 |
Width: 44 |
|
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:
diff
changeset
|
121 |
VWidth: 1670 |
|
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:
diff
changeset
|
122 |
Flags: HW |
|
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:
diff
changeset
|
123 |
LayerCount: 2 |
|
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:
diff
changeset
|
124 |
Fore |
|
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:
diff
changeset
|
125 |
SplineSet |
|
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:
diff
changeset
|
126 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
127 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
128 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
129 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
130 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
131 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
132 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
133 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
134 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
135 |
EndSplineSet |
|
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:
diff
changeset
|
136 |
EndChar |
|
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:
diff
changeset
|
137 |
|
|
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:
diff
changeset
|
138 |
StartChar: uni21D7 |
|
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:
diff
changeset
|
139 |
Encoding: 8663 8663 4 |
|
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:
diff
changeset
|
140 |
Width: 44 |
|
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:
diff
changeset
|
141 |
VWidth: 1670 |
|
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:
diff
changeset
|
142 |
Flags: HW |
|
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:
diff
changeset
|
143 |
LayerCount: 2 |
|
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:
diff
changeset
|
144 |
Fore |
|
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:
diff
changeset
|
145 |
SplineSet |
|
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:
diff
changeset
|
146 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
147 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
148 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
149 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
150 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
151 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
152 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
153 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
154 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
155 |
EndSplineSet |
|
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:
diff
changeset
|
156 |
EndChar |
|
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:
diff
changeset
|
157 |
|
|
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:
diff
changeset
|
158 |
StartChar: uni21D8 |
|
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:
diff
changeset
|
159 |
Encoding: 8664 8664 5 |
|
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:
diff
changeset
|
160 |
Width: 44 |
|
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:
diff
changeset
|
161 |
VWidth: 1670 |
|
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:
diff
changeset
|
162 |
Flags: HW |
|
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:
diff
changeset
|
163 |
LayerCount: 2 |
|
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:
diff
changeset
|
164 |
Fore |
|
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:
diff
changeset
|
165 |
SplineSet |
|
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:
diff
changeset
|
166 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
167 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
168 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
169 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
170 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
171 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
172 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
173 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
174 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
175 |
EndSplineSet |
|
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:
diff
changeset
|
176 |
EndChar |
|
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:
diff
changeset
|
177 |
|
|
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:
diff
changeset
|
178 |
StartChar: uni21D9 |
|
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:
diff
changeset
|
179 |
Encoding: 8665 8665 6 |
|
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:
diff
changeset
|
180 |
Width: 44 |
|
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:
diff
changeset
|
181 |
VWidth: 1670 |
|
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:
diff
changeset
|
182 |
Flags: HW |
|
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:
diff
changeset
|
183 |
LayerCount: 2 |
|
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:
diff
changeset
|
184 |
Fore |
|
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:
diff
changeset
|
185 |
SplineSet |
|
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:
diff
changeset
|
186 |
33.4502 5 m 128 |
|
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:
diff
changeset
|
187 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
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:
diff
changeset
|
188 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
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:
diff
changeset
|
189 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
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:
diff
changeset
|
190 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
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:
diff
changeset
|
191 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
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:
diff
changeset
|
192 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
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:
diff
changeset
|
193 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
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:
diff
changeset
|
194 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
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:
diff
changeset
|
195 |
EndSplineSet |
|
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:
diff
changeset
|
196 |
EndChar |
|
67255
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
197 |
|
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
198 |
StartChar: backslash |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
199 |
Encoding: 92 92 7 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
200 |
Width: 44 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
201 |
VWidth: 1670 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
202 |
Flags: HW |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
203 |
LayerCount: 2 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
204 |
Fore |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
205 |
SplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
206 |
33.4502 5 m 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
207 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
208 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
209 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
210 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
211 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
212 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
213 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
214 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
215 |
EndSplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
216 |
EndChar |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
217 |
|
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
218 |
StartChar: less |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
219 |
Encoding: 60 60 8 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
220 |
Width: 44 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
221 |
VWidth: 1670 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
222 |
Flags: HW |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
223 |
LayerCount: 2 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
224 |
Fore |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
225 |
SplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
226 |
33.4502 5 m 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
227 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
228 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
229 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
230 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
231 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
232 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
233 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
234 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
235 |
EndSplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
236 |
EndChar |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
237 |
|
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
238 |
StartChar: greater |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
239 |
Encoding: 62 62 9 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
240 |
Width: 44 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
241 |
VWidth: 1670 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
242 |
Flags: HW |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
243 |
LayerCount: 2 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
244 |
Fore |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
245 |
SplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
246 |
33.4502 5 m 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
247 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
248 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
249 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
250 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
251 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
252 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
253 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
254 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
255 |
EndSplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
256 |
EndChar |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
257 |
|
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
258 |
StartChar: asciicircum |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
259 |
Encoding: 94 94 10 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
260 |
Width: 44 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
261 |
VWidth: 1670 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
262 |
Flags: HW |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
263 |
LayerCount: 2 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
264 |
Fore |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
265 |
SplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
266 |
33.4502 5 m 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
267 |
33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
268 |
27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
269 |
18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
270 |
11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
271 |
9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
272 |
15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
273 |
24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
274 |
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128 |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
275 |
EndSplineSet |
|
f1f983484878
HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents:
63683
diff
changeset
|
276 |
EndChar |
|
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:
diff
changeset
|
277 |
EndChars |
|
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:
diff
changeset
|
278 |
EndSplineFont |