# HG changeset patch # User wenzelm # Date 1471035105 -7200 # Node ID 87c6158f4ef45ce5a1f46cf395783a2fbc2a56df # Parent 67cffbbca84d6d11227c6f63a752807d5bc12063 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; diff -r 67cffbbca84d -r 87c6158f4ef4 Admin/components/components.sha1 --- 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 diff -r 67cffbbca84d -r 87c6158f4ef4 Admin/components/main --- 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 diff -r 67cffbbca84d -r 87c6158f4ef4 etc/isabelle.css --- 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; } diff -r 67cffbbca84d -r 87c6158f4ef4 lib/fonts/Vacuous.sfd --- /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 diff -r 67cffbbca84d -r 87c6158f4ef4 src/Pure/Thy/present.scala --- 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) } } }