HTML rendering of \<^control> as in Isabelle/jEdit;
authorwenzelm
Fri Dec 22 15:49:44 2017 +0100 (20 months ago)
changeset 67255f1f983484878
parent 67254 31dd98471e88
child 67256 ce7d856680d1
HTML rendering of \<^control> as in Isabelle/jEdit;
Admin/components/components.sha1
Admin/components/main
etc/isabelle.css
lib/fonts/Vacuous.sfd
src/Pure/General/symbol.scala
src/Pure/Thy/html.scala
     1.1 --- a/Admin/components/components.sha1	Fri Dec 22 14:35:29 2017 +0100
     1.2 +++ b/Admin/components/components.sha1	Fri Dec 22 15:49:44 2017 +0100
     1.3 @@ -63,6 +63,7 @@
     1.4  8ff0eedf0191d808ecc58c6b3149a4697f29ab21  isabelle_fonts-20160812-1.tar.gz
     1.5  9283e3b0b4c7239f57b18e076ec8bb21021832cb  isabelle_fonts-20160812.tar.gz
     1.6  620cffeb125e198b91a716da116f754d6cc8174b  isabelle_fonts-20160830.tar.gz
     1.7 +b70690c85c05d0ca5bc29287abd20142f6ddcfb0  isabelle_fonts-20171222.tar.gz
     1.8  8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
     1.9  38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
    1.10  d765bc4ad2f34d494429b2a8c1563c49db224944  jdk-7u13.tar.gz
     2.1 --- a/Admin/components/main	Fri Dec 22 14:35:29 2017 +0100
     2.2 +++ b/Admin/components/main	Fri Dec 22 15:49:44 2017 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  csdp-6.x
     2.5  cvc4-1.5-3
     2.6  e-2.0-1
     2.7 -isabelle_fonts-20160830
     2.8 +isabelle_fonts-20171222
     2.9  jdk-8u152
    2.10  jedit_build-20170319
    2.11  jfreechart-1.0.14-1
     3.1 --- a/etc/isabelle.css	Fri Dec 22 14:35:29 2017 +0100
     3.2 +++ b/etc/isabelle.css	Fri Dec 22 15:49:44 2017 +0100
     3.3 @@ -31,6 +31,7 @@
     3.4  /* basic syntax markup */
     3.5  
     3.6  .hidden         { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); }
     3.7 +.control        { font-weight: bold; font-style: italic; }
     3.8  
     3.9  .binding        { color: #336655; }
    3.10  .tfree          { color: #A020F0; }
     4.1 --- a/lib/fonts/Vacuous.sfd	Fri Dec 22 14:35:29 2017 +0100
     4.2 +++ b/lib/fonts/Vacuous.sfd	Fri Dec 22 15:49:44 2017 +0100
     4.3 @@ -20,7 +20,7 @@
     4.4  OS2_WeightWidthSlopeOnly: 0
     4.5  OS2_UseTypoMetrics: 1
     4.6  CreationTime: 1471028867
     4.7 -ModificationTime: 1471030389
     4.8 +ModificationTime: 1513953645
     4.9  PfmFamily: 17
    4.10  TTFWeight: 500
    4.11  TTFWidth: 5
    4.12 @@ -49,11 +49,11 @@
    4.13  DisplaySize: -96
    4.14  AntiAlias: 1
    4.15  FitToEm: 1
    4.16 -WinInfo: 8560 20 14
    4.17 +WinInfo: 0 20 14
    4.18  BeginPrivate: 0
    4.19  EndPrivate
    4.20  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.21 -BeginChars: 1114112 7
    4.22 +BeginChars: 1114112 11
    4.23  
    4.24  StartChar: uni2759
    4.25  Encoding: 10073 10073 0
    4.26 @@ -194,5 +194,85 @@
    4.27   32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
    4.28  EndSplineSet
    4.29  EndChar
    4.30 +
    4.31 +StartChar: backslash
    4.32 +Encoding: 92 92 7
    4.33 +Width: 44
    4.34 +VWidth: 1670
    4.35 +Flags: HW
    4.36 +LayerCount: 2
    4.37 +Fore
    4.38 +SplineSet
    4.39 +33.4502 5 m 128
    4.40 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
    4.41 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
    4.42 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
    4.43 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
    4.44 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
    4.45 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
    4.46 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
    4.47 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
    4.48 +EndSplineSet
    4.49 +EndChar
    4.50 +
    4.51 +StartChar: less
    4.52 +Encoding: 60 60 8
    4.53 +Width: 44
    4.54 +VWidth: 1670
    4.55 +Flags: HW
    4.56 +LayerCount: 2
    4.57 +Fore
    4.58 +SplineSet
    4.59 +33.4502 5 m 128
    4.60 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
    4.61 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
    4.62 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
    4.63 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
    4.64 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
    4.65 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
    4.66 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
    4.67 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
    4.68 +EndSplineSet
    4.69 +EndChar
    4.70 +
    4.71 +StartChar: greater
    4.72 +Encoding: 62 62 9
    4.73 +Width: 44
    4.74 +VWidth: 1670
    4.75 +Flags: HW
    4.76 +LayerCount: 2
    4.77 +Fore
    4.78 +SplineSet
    4.79 +33.4502 5 m 128
    4.80 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
    4.81 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
    4.82 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
    4.83 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
    4.84 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
    4.85 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
    4.86 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
    4.87 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
    4.88 +EndSplineSet
    4.89 +EndChar
    4.90 +
    4.91 +StartChar: asciicircum
    4.92 +Encoding: 94 94 10
    4.93 +Width: 44
    4.94 +VWidth: 1670
    4.95 +Flags: HW
    4.96 +LayerCount: 2
    4.97 +Fore
    4.98 +SplineSet
    4.99 +33.4502 5 m 128
   4.100 + 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
   4.101 + 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
   4.102 + 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
   4.103 + 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
   4.104 + 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
   4.105 + 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
   4.106 + 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
   4.107 + 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
   4.108 +EndSplineSet
   4.109 +EndChar
   4.110  EndChars
   4.111  EndSplineFont
     5.1 --- a/src/Pure/General/symbol.scala	Fri Dec 22 14:35:29 2017 +0100
     5.2 +++ b/src/Pure/General/symbol.scala	Fri Dec 22 15:49:44 2017 +0100
     5.3 @@ -583,6 +583,11 @@
     5.4    val control_prefix = "\\<^"
     5.5    val control_suffix = ">"
     5.6  
     5.7 +  def control_name(sym: Symbol): Option[String] =
     5.8 +    if (is_control_encoded(sym))
     5.9 +      Some(sym.substring(control_prefix.length, sym.length - control_suffix.length))
    5.10 +    else None
    5.11 +
    5.12    def is_control_encoded(sym: Symbol): Boolean =
    5.13      sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
    5.14  
     6.1 --- a/src/Pure/Thy/html.scala	Fri Dec 22 14:35:29 2017 +0100
     6.2 +++ b/src/Pure/Thy/html.scala	Fri Dec 22 15:49:44 2017 +0100
     6.3 @@ -56,7 +56,14 @@
     6.4            case Some(html) =>
     6.5              output_hidden(output_string(sym)); s ++= html
     6.6            case None =>
     6.7 -            output_string(sym)
     6.8 +            if (hidden && Symbol.is_control_encoded(sym)) {
     6.9 +              output_hidden(output_string(Symbol.control_prefix))
    6.10 +              s ++= "<span class=\"control\">"
    6.11 +              output_string(Symbol.control_name(sym).get)
    6.12 +              s ++= "</span>"
    6.13 +              output_hidden(output_string(Symbol.control_suffix))
    6.14 +            }
    6.15 +            else output_string(sym)
    6.16          }
    6.17        }
    6.18