# HG changeset patch
# User wenzelm
# Date 1513954184 -3600
# Node ID f1f9834848784a36e3aeb8fc1d4ceb2a66770cda
# Parent  31dd98471e886a2ecb45388a888e1b4dcb0ae913
HTML rendering of \<^control> as in Isabelle/jEdit;

diff -r 31dd98471e88 -r f1f983484878 Admin/components/components.sha1
--- 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
diff -r 31dd98471e88 -r f1f983484878 Admin/components/main
--- 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
diff -r 31dd98471e88 -r f1f983484878 etc/isabelle.css
--- 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; }
diff -r 31dd98471e88 -r f1f983484878 lib/fonts/Vacuous.sfd
--- 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
diff -r 31dd98471e88 -r f1f983484878 src/Pure/General/symbol.scala
--- 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)
 
diff -r 31dd98471e88 -r f1f983484878 src/Pure/Thy/html.scala
--- 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)
         }
       }