more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
authorwenzelm
Fri Aug 12 22:51:45 2016 +0200 (2016-08-12)
changeset 6368387c6158f4ef4
parent 63682 67cffbbca84d
child 63684 905d3fc815ff
more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
Admin/components/components.sha1
Admin/components/main
etc/isabelle.css
lib/fonts/Vacuous.sfd
src/Pure/Thy/present.scala
     1.1 --- a/Admin/components/components.sha1	Fri Aug 12 20:58:20 2016 +0200
     1.2 +++ b/Admin/components/components.sha1	Fri Aug 12 22:51:45 2016 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4  1f004a6bf20088a7e8f1b3d4153aa85de6fc1091  isabelle_fonts-20160101.tar.gz
     1.5  379d51ef3b71452dac34ba905def3daa8b590f2e  isabelle_fonts-20160102.tar.gz
     1.6  878536aab1eaf1a52da560c20bb41ab942971fa3  isabelle_fonts-20160227.tar.gz
     1.7 +8ff0eedf0191d808ecc58c6b3149a4697f29ab21  isabelle_fonts-20160812-1.tar.gz
     1.8  9283e3b0b4c7239f57b18e076ec8bb21021832cb  isabelle_fonts-20160812.tar.gz
     1.9  8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
    1.10  38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
     2.1 --- a/Admin/components/main	Fri Aug 12 20:58:20 2016 +0200
     2.2 +++ b/Admin/components/main	Fri Aug 12 22:51:45 2016 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  cvc4-1.5pre-3
     2.5  e-1.8
     2.6  Haskabelle-2015
     2.7 -isabelle_fonts-20160812
     2.8 +isabelle_fonts-20160812-1
     2.9  jdk-8u102
    2.10  jedit_build-20160330
    2.11  jfreechart-1.0.14-1
     3.1 --- a/etc/isabelle.css	Fri Aug 12 20:58:20 2016 +0200
     3.2 +++ b/etc/isabelle.css	Fri Aug 12 22:51:45 2016 +0200
     3.3 @@ -11,6 +11,11 @@
     3.4    font-weight: bold;
     3.5  }
     3.6  
     3.7 +@font-face {
     3.8 +  font-family: 'Vacuous';
     3.9 +  src: url('Vacuous.ttf') format('truetype');
    3.10 +}
    3.11 +
    3.12  body { background-color: #FFFFFF; }
    3.13  
    3.14  .head     { background-color: #FFFFFF; }
    3.15 @@ -31,7 +36,7 @@
    3.16  
    3.17  /* basic syntax markup */
    3.18  
    3.19 -.hidden         { font-size: 1px; visibility: hidden; }
    3.20 +.hidden         { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); }
    3.21  
    3.22  .binding        { color: #336655; }
    3.23  .tfree          { color: #A020F0; }
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/lib/fonts/Vacuous.sfd	Fri Aug 12 22:51:45 2016 +0200
     4.3 @@ -0,0 +1,198 @@
     4.4 +SplineFontDB: 3.0
     4.5 +FontName: Vacuous
     4.6 +FullName: Vacuous
     4.7 +FamilyName: Vacuous
     4.8 +Weight: Medium
     4.9 +Copyright: 
    4.10 +UComments: "2016-8-12: Created." 
    4.11 +Version: 001.000
    4.12 +ItalicAngle: 0
    4.13 +UnderlinePosition: -100
    4.14 +UnderlineWidth: 50
    4.15 +Ascent: 800
    4.16 +Descent: 200
    4.17 +LayerCount: 2
    4.18 +Layer: 0 0 "Back"  1
    4.19 +Layer: 1 0 "Fore"  0
    4.20 +XUID: [1021 906 1711068302 5949507]
    4.21 +FSType: 8
    4.22 +OS2Version: 0
    4.23 +OS2_WeightWidthSlopeOnly: 0
    4.24 +OS2_UseTypoMetrics: 1
    4.25 +CreationTime: 1471028867
    4.26 +ModificationTime: 1471030389
    4.27 +PfmFamily: 17
    4.28 +TTFWeight: 500
    4.29 +TTFWidth: 5
    4.30 +LineGap: 90
    4.31 +VLineGap: 0
    4.32 +OS2TypoAscent: 0
    4.33 +OS2TypoAOffset: 1
    4.34 +OS2TypoDescent: 0
    4.35 +OS2TypoDOffset: 1
    4.36 +OS2TypoLinegap: 90
    4.37 +OS2WinAscent: 0
    4.38 +OS2WinAOffset: 1
    4.39 +OS2WinDescent: 0
    4.40 +OS2WinDOffset: 1
    4.41 +HheadAscent: 0
    4.42 +HheadAOffset: 1
    4.43 +HheadDescent: 0
    4.44 +HheadDOffset: 1
    4.45 +OS2Vendor: 'PfEd'
    4.46 +MarkAttachClasses: 1
    4.47 +DEI: 91125
    4.48 +LangName: 1033 
    4.49 +Encoding: UnicodeFull
    4.50 +UnicodeInterp: none
    4.51 +NameList: Adobe Glyph List
    4.52 +DisplaySize: -96
    4.53 +AntiAlias: 1
    4.54 +FitToEm: 1
    4.55 +WinInfo: 8560 20 14
    4.56 +BeginPrivate: 0
    4.57 +EndPrivate
    4.58 +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
    4.59 +BeginChars: 1114112 7
    4.60 +
    4.61 +StartChar: uni2759
    4.62 +Encoding: 10073 10073 0
    4.63 +Width: 44
    4.64 +VWidth: 1670
    4.65 +Flags: HW
    4.66 +LayerCount: 2
    4.67 +Fore
    4.68 +SplineSet
    4.69 +33.4502 5 m 128
    4.70 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
    4.71 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
    4.72 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
    4.73 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
    4.74 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
    4.75 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
    4.76 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
    4.77 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
    4.78 +EndSplineSet
    4.79 +EndChar
    4.80 +
    4.81 +StartChar: uni21E9
    4.82 +Encoding: 8681 8681 1
    4.83 +Width: 44
    4.84 +VWidth: 1670
    4.85 +Flags: HW
    4.86 +LayerCount: 2
    4.87 +Fore
    4.88 +SplineSet
    4.89 +33.4502 5 m 128
    4.90 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
    4.91 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
    4.92 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
    4.93 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
    4.94 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
    4.95 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
    4.96 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
    4.97 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
    4.98 +EndSplineSet
    4.99 +EndChar
   4.100 +
   4.101 +StartChar: uni21E7
   4.102 +Encoding: 8679 8679 2
   4.103 +Width: 44
   4.104 +VWidth: 1670
   4.105 +Flags: HW
   4.106 +LayerCount: 2
   4.107 +Fore
   4.108 +SplineSet
   4.109 +33.4502 5 m 128
   4.110 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
   4.111 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
   4.112 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
   4.113 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
   4.114 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
   4.115 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
   4.116 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
   4.117 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
   4.118 +EndSplineSet
   4.119 +EndChar
   4.120 +
   4.121 +StartChar: uni21D6
   4.122 +Encoding: 8662 8662 3
   4.123 +Width: 44
   4.124 +VWidth: 1670
   4.125 +Flags: HW
   4.126 +LayerCount: 2
   4.127 +Fore
   4.128 +SplineSet
   4.129 +33.4502 5 m 128
   4.130 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
   4.131 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
   4.132 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
   4.133 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
   4.134 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
   4.135 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
   4.136 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
   4.137 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
   4.138 +EndSplineSet
   4.139 +EndChar
   4.140 +
   4.141 +StartChar: uni21D7
   4.142 +Encoding: 8663 8663 4
   4.143 +Width: 44
   4.144 +VWidth: 1670
   4.145 +Flags: HW
   4.146 +LayerCount: 2
   4.147 +Fore
   4.148 +SplineSet
   4.149 +33.4502 5 m 128
   4.150 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
   4.151 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
   4.152 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
   4.153 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
   4.154 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
   4.155 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
   4.156 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
   4.157 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
   4.158 +EndSplineSet
   4.159 +EndChar
   4.160 +
   4.161 +StartChar: uni21D8
   4.162 +Encoding: 8664 8664 5
   4.163 +Width: 44
   4.164 +VWidth: 1670
   4.165 +Flags: HW
   4.166 +LayerCount: 2
   4.167 +Fore
   4.168 +SplineSet
   4.169 +33.4502 5 m 128
   4.170 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
   4.171 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
   4.172 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
   4.173 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
   4.174 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
   4.175 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
   4.176 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
   4.177 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
   4.178 +EndSplineSet
   4.179 +EndChar
   4.180 +
   4.181 +StartChar: uni21D9
   4.182 +Encoding: 8665 8665 6
   4.183 +Width: 44
   4.184 +VWidth: 1670
   4.185 +Flags: HW
   4.186 +LayerCount: 2
   4.187 +Fore
   4.188 +SplineSet
   4.189 +33.4502 5 m 128
   4.190 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
   4.191 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
   4.192 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
   4.193 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
   4.194 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
   4.195 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
   4.196 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
   4.197 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
   4.198 +EndSplineSet
   4.199 +EndChar
   4.200 +EndChars
   4.201 +EndSplineFont
     5.1 --- a/src/Pure/Thy/present.scala	Fri Aug 12 20:58:20 2016 +0200
     5.2 +++ b/src/Pure/Thy/present.scala	Fri Aug 12 22:51:45 2016 +0200
     5.3 @@ -112,6 +112,8 @@
     5.4  
     5.5        for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
     5.6          File.copy(font, session_prefix)
     5.7 +      for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS_HTML")))
     5.8 +        File.copy(font, session_prefix)
     5.9      }
    5.10    }
    5.11  }