--- a/Admin/components/components.sha1 Fri Dec 22 14:35:29 2017 +0100
+++ b/Admin/components/components.sha1 Fri Dec 22 15:49:44 2017 +0100
@@ -63,6 +63,7 @@
8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz
9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz
620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz
+b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
--- a/Admin/components/main Fri Dec 22 14:35:29 2017 +0100
+++ b/Admin/components/main Fri Dec 22 15:49:44 2017 +0100
@@ -4,7 +4,7 @@
csdp-6.x
cvc4-1.5-3
e-2.0-1
-isabelle_fonts-20160830
+isabelle_fonts-20171222
jdk-8u152
jedit_build-20170319
jfreechart-1.0.14-1
--- a/etc/isabelle.css Fri Dec 22 14:35:29 2017 +0100
+++ b/etc/isabelle.css Fri Dec 22 15:49:44 2017 +0100
@@ -31,6 +31,7 @@
/* basic syntax markup */
.hidden { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); }
+.control { font-weight: bold; font-style: italic; }
.binding { color: #336655; }
.tfree { color: #A020F0; }
--- a/lib/fonts/Vacuous.sfd Fri Dec 22 14:35:29 2017 +0100
+++ b/lib/fonts/Vacuous.sfd Fri Dec 22 15:49:44 2017 +0100
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1471028867
-ModificationTime: 1471030389
+ModificationTime: 1513953645
PfmFamily: 17
TTFWeight: 500
TTFWidth: 5
@@ -49,11 +49,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 8560 20 14
+WinInfo: 0 20 14
BeginPrivate: 0
EndPrivate
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
-BeginChars: 1114112 7
+BeginChars: 1114112 11
StartChar: uni2759
Encoding: 10073 10073 0
@@ -194,5 +194,85 @@
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
EndSplineSet
EndChar
+
+StartChar: backslash
+Encoding: 92 92 7
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
+
+StartChar: less
+Encoding: 60 60 8
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
+
+StartChar: greater
+Encoding: 62 62 9
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
+
+StartChar: asciicircum
+Encoding: 94 94 10
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/src/Pure/General/symbol.scala Fri Dec 22 14:35:29 2017 +0100
+++ b/src/Pure/General/symbol.scala Fri Dec 22 15:49:44 2017 +0100
@@ -583,6 +583,11 @@
val control_prefix = "\\<^"
val control_suffix = ">"
+ def control_name(sym: Symbol): Option[String] =
+ if (is_control_encoded(sym))
+ Some(sym.substring(control_prefix.length, sym.length - control_suffix.length))
+ else None
+
def is_control_encoded(sym: Symbol): Boolean =
sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
--- a/src/Pure/Thy/html.scala Fri Dec 22 14:35:29 2017 +0100
+++ b/src/Pure/Thy/html.scala Fri Dec 22 15:49:44 2017 +0100
@@ -56,7 +56,14 @@
case Some(html) =>
output_hidden(output_string(sym)); s ++= html
case None =>
- output_string(sym)
+ if (hidden && Symbol.is_control_encoded(sym)) {
+ output_hidden(output_string(Symbol.control_prefix))
+ s ++= "<span class=\"control\">"
+ output_string(Symbol.control_name(sym).get)
+ s ++= "</span>"
+ output_hidden(output_string(Symbol.control_suffix))
+ }
+ else output_string(sym)
}
}