lib/fonts/Vacuous.sfd
author wenzelm
Wed, 26 Sep 2018 22:07:35 +0200
changeset 69073 d05defa39e3d
parent 67255 f1f983484878
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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