more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;

--- a/Admin/components/components.sha1	Fri Aug 12 20:58:20 2016 +0200
+++ b/Admin/components/components.sha1	Fri Aug 12 22:51:45 2016 +0200
@@ -46,6 +46,7 @@
 1f004a6bf20088a7e8f1b3d4153aa85de6fc1091  isabelle_fonts-20160101.tar.gz
 379d51ef3b71452dac34ba905def3daa8b590f2e  isabelle_fonts-20160102.tar.gz
 878536aab1eaf1a52da560c20bb41ab942971fa3  isabelle_fonts-20160227.tar.gz
+8ff0eedf0191d808ecc58c6b3149a4697f29ab21  isabelle_fonts-20160812-1.tar.gz
 9283e3b0b4c7239f57b18e076ec8bb21021832cb  isabelle_fonts-20160812.tar.gz
 8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
 38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz

--- a/Admin/components/main	Fri Aug 12 20:58:20 2016 +0200
+++ b/Admin/components/main	Fri Aug 12 22:51:45 2016 +0200
@@ -4,7 +4,7 @@
 cvc4-1.5pre-3
 e-1.8
 Haskabelle-2015
-isabelle_fonts-20160812
+isabelle_fonts-20160812-1
 jdk-8u102
 jedit_build-20160330
 jfreechart-1.0.14-1

--- a/etc/isabelle.css	Fri Aug 12 20:58:20 2016 +0200
+++ b/etc/isabelle.css	Fri Aug 12 22:51:45 2016 +0200
@@ -11,6 +11,11 @@
   font-weight: bold;
 }
 
+@font-face {
+  font-family: 'Vacuous';
+  src: url('Vacuous.ttf') format('truetype');
+}
+
 body { background-color: #FFFFFF; }
 
 .head     { background-color: #FFFFFF; }
@@ -31,7 +36,7 @@
 
 /* basic syntax markup */
 
-.hidden         { font-size: 1px; visibility: hidden; }
+.hidden         { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); }
 
 .binding        { color: #336655; }
 .tfree          { color: #A020F0; }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/fonts/Vacuous.sfd	Fri Aug 12 22:51:45 2016 +0200
@@ -0,0 +1,198 @@
+SplineFontDB: 3.0
+FontName: Vacuous
+FullName: Vacuous
+FamilyName: Vacuous
+Weight: Medium
+Copyright: 
+UComments: "2016-8-12: Created." 
+Version: 001.000
+ItalicAngle: 0
+UnderlinePosition: -100
+UnderlineWidth: 50
+Ascent: 800
+Descent: 200
+LayerCount: 2
+Layer: 0 0 "Back"  1
+Layer: 1 0 "Fore"  0
+XUID: [1021 906 1711068302 5949507]
+FSType: 8
+OS2Version: 0
+OS2_WeightWidthSlopeOnly: 0
+OS2_UseTypoMetrics: 1
+CreationTime: 1471028867
+ModificationTime: 1471030389
+PfmFamily: 17
+TTFWeight: 500
+TTFWidth: 5
+LineGap: 90
+VLineGap: 0
+OS2TypoAscent: 0
+OS2TypoAOffset: 1
+OS2TypoDescent: 0
+OS2TypoDOffset: 1
+OS2TypoLinegap: 90
+OS2WinAscent: 0
+OS2WinAOffset: 1
+OS2WinDescent: 0
+OS2WinDOffset: 1
+HheadAscent: 0
+HheadAOffset: 1
+HheadDescent: 0
+HheadDOffset: 1
+OS2Vendor: 'PfEd'
+MarkAttachClasses: 1
+DEI: 91125
+LangName: 1033 
+Encoding: UnicodeFull
+UnicodeInterp: none
+NameList: Adobe Glyph List
+DisplaySize: -96
+AntiAlias: 1
+FitToEm: 1
+WinInfo: 8560 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
+
+StartChar: uni2759
+Encoding: 10073 10073 0
+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: uni21E9
+Encoding: 8681 8681 1
+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: uni21E7
+Encoding: 8679 8679 2
+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: uni21D6
+Encoding: 8662 8662 3
+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: uni21D7
+Encoding: 8663 8663 4
+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: uni21D8
+Encoding: 8664 8664 5
+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: uni21D9
+Encoding: 8665 8665 6
+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/Thy/present.scala	Fri Aug 12 20:58:20 2016 +0200
+++ b/src/Pure/Thy/present.scala	Fri Aug 12 22:51:45 2016 +0200
@@ -112,6 +112,8 @@
 
       for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
         File.copy(font, session_prefix)
+      for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS_HTML")))
+        File.copy(font, session_prefix)
     }
   }
 }