more arrow symbols;
authorwenzelm
Tue Dec 29 21:51:58 2015 +0100 (2015-12-29)
changeset 6196437a0cbee00c2
parent 61963 2548e7cc86fb
child 61965 a35d141e6c75
more arrow symbols;
NEWS
etc/symbols
lib/fonts/IsabelleText.sfd
lib/fonts/IsabelleTextBold.sfd
lib/texinputs/isabellesym.sty
     1.1 --- a/NEWS	Tue Dec 29 20:58:18 2015 +0100
     1.2 +++ b/NEWS	Tue Dec 29 21:51:58 2015 +0100
     1.3 @@ -31,17 +31,8 @@
     1.4  remains available under print mode "ASCII", but less important syntax
     1.5  has been removed (see below).
     1.6  
     1.7 -* Support for arrows of various lengths, with rendering in LaTeX and
     1.8 -Isabelle fonts:
     1.9 -
    1.10 -  \<leftarrow>
    1.11 -  \<longleftarrow>
    1.12 -  \<longlongleftarrow>
    1.13 -  \<longlonglongleftarrow>
    1.14 -  \<rightarrow>
    1.15 -  \<longrightarrow>
    1.16 -  \<longlongrightarrow>
    1.17 -  \<longlonglongrightarrow>
    1.18 +* Support for more arrow symbols, with rendering in LaTeX and
    1.19 +Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
    1.20  
    1.21  
    1.22  *** Prover IDE -- Isabelle/Scala/jEdit ***
     2.1 --- a/etc/symbols	Tue Dec 29 20:58:18 2015 +0100
     2.2 +++ b/etc/symbols	Tue Dec 29 21:51:58 2015 +0100
     2.3 @@ -164,8 +164,10 @@
     2.4  \<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: ---->
     2.5  \<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
     2.6  \<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
     2.7 +\<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.
     2.8  \<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>
     2.9  \<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: .>  abbrev: ==>
    2.10 +\<Rrightarrow>          code: 0x0021db  group: arrow  abbrev: .>
    2.11  \<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <>  abbrev: <->
    2.12  \<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <>  abbrev: <->  abbrev: <-->
    2.13  \<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <>
     3.1 --- a/lib/fonts/IsabelleText.sfd	Tue Dec 29 20:58:18 2015 +0100
     3.2 +++ b/lib/fonts/IsabelleText.sfd	Tue Dec 29 21:51:58 2015 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4  OS2_WeightWidthSlopeOnly: 0
     3.5  OS2_UseTypoMetrics: 1
     3.6  CreationTime: 1050361371
     3.7 -ModificationTime: 1451417325
     3.8 +ModificationTime: 1451421536
     3.9  PfmFamily: 17
    3.10  TTFWeight: 400
    3.11  TTFWidth: 5
    3.12 @@ -2241,12 +2241,12 @@
    3.13  DisplaySize: -96
    3.14  AntiAlias: 1
    3.15  FitToEm: 1
    3.16 -WinInfo: 10278 18 16
    3.17 +WinInfo: 8532 18 16
    3.18  BeginPrivate: 0
    3.19  EndPrivate
    3.20  TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
    3.21 -BeginChars: 1114189 1399
    3.22 -
    3.23 +BeginChars: 1114189 1401
    3.24 +
    3.25  StartChar: u10000
    3.26  Encoding: 65536 65536 0
    3.27  AltUni2: 010000.ffffffff.0
    3.28 @@ -62245,5 +62245,98 @@
    3.29   2694 511.5 l 6,0,-1
    3.30  EndSplineSet
    3.31  EndChar
    3.32 +
    3.33 +StartChar: uni21DA
    3.34 +Encoding: 8666 8666 1399
    3.35 +Width: 2174
    3.36 +VWidth: 2210
    3.37 +Flags: W
    3.38 +HStem: 70.0199 88.7998<756.22 2048.24> 500.7 88.8008<332.2 2048.26> 931.38 88.7998<756.22 2048.24>
    3.39 +LayerCount: 2
    3.40 +Fore
    3.41 +SplineSet
    3.42 +1970.56 500.7 m 2,0,-1
    3.43 + 332.2 500.7 l 1,1,2
    3.44 + 512.02 378.6 512.02 378.6 674.08 181.02 c 0,3,4
    3.45 + 687.4 165.479 687.4 165.479 696.28 162.149 c 128,-1,5
    3.46 + 705.16 158.819 705.16 158.819 736.24 158.819 c 2,6,-1
    3.47 + 1968.34 158.819 l 2,7,8
    3.48 + 2048.26 158.819 2048.26 158.819 2048.26 114.42 c 0,9,10
    3.49 + 2048.26 94.4395 2048.26 94.4395 2034.94 83.3398 c 128,-1,11
    3.50 + 2021.62 72.2393 2021.62 72.2393 2008.3 71.1299 c 128,-1,12
    3.51 + 1994.98 70.0195 1994.98 70.0195 1970.56 70.0195 c 2,13,-1
    3.52 + 756.22 70.0195 l 1,14,15
    3.53 + 860.56 -100.92 860.56 -100.92 916.06 -256.32 c 1,16,-1
    3.54 + 811.72 -256.32 l 1,17,18
    3.55 + 625.24 269.82 625.24 269.82 125.74 545.1 c 1,19,20
    3.56 + 625.24 818.16 625.24 818.16 811.72 1346.52 c 1,21,-1
    3.57 + 916.06 1346.52 l 1,22,23
    3.58 + 865 1200 865 1200 756.22 1020.18 c 1,24,-1
    3.59 + 1970.56 1020.18 l 2,25,26
    3.60 + 1994.98 1020.18 1994.98 1020.18 2008.3 1019.07 c 128,-1,27
    3.61 + 2021.62 1017.96 2021.62 1017.96 2034.94 1006.86 c 128,-1,28
    3.62 + 2048.26 995.76 2048.26 995.76 2048.26 975.78 c 0,29,30
    3.63 + 2048.26 931.38 2048.26 931.38 1968.34 931.38 c 2,31,-1
    3.64 + 736.24 931.38 l 2,32,33
    3.65 + 705.16 931.38 705.16 931.38 696.28 928.05 c 128,-1,34
    3.66 + 687.4 924.72 687.4 924.72 674.08 906.96 c 0,35,36
    3.67 + 507.58 707.16 507.58 707.16 332.2 589.5 c 1,37,-1
    3.68 + 1970.56 589.5 l 2,38,39
    3.69 + 1994.98 589.5 1994.98 589.5 2008.3 588.39 c 128,-1,40
    3.70 + 2021.62 587.28 2021.62 587.28 2034.94 576.18 c 128,-1,41
    3.71 + 2048.26 565.08 2048.26 565.08 2048.26 545.1 c 128,-1,42
    3.72 + 2048.26 525.12 2048.26 525.12 2036.05 514.02 c 128,-1,43
    3.73 + 2023.84 502.92 2023.84 502.92 2010.52 501.81 c 128,-1,44
    3.74 + 1997.2 500.7 1997.2 500.7 1970.56 500.7 c 2,0,-1
    3.75 +EndSplineSet
    3.76 +EndChar
    3.77 +
    3.78 +StartChar: uni21DB
    3.79 +Encoding: 8667 8667 1400
    3.80 +Width: 2179
    3.81 +VWidth: 2210
    3.82 +Flags: W
    3.83 +HStem: 70.0199 88.7998<127.743 1419.78> 500.7 88.8008<127.745 1843.8> 931.38 88.7998<127.743 1419.78>
    3.84 +LayerCount: 2
    3.85 +Fore
    3.86 +SplineSet
    3.87 +1439.76 931.38 m 2,0,-1
    3.88 + 205.44 931.38 l 2,1,2
    3.89 + 181.021 931.38 181.021 931.38 167.7 932.49 c 128,-1,3
    3.90 + 154.38 933.6 154.38 933.6 141.061 944.7 c 128,-1,4
    3.91 + 127.74 955.8 127.74 955.8 127.74 975.78 c 128,-1,5
    3.92 + 127.74 995.76 127.74 995.76 139.95 1006.86 c 128,-1,6
    3.93 + 152.16 1017.96 152.16 1017.96 165.48 1019.07 c 128,-1,7
    3.94 + 178.8 1020.18 178.8 1020.18 205.44 1020.18 c 2,8,-1
    3.95 + 1419.78 1020.18 l 1,9,10
    3.96 + 1315.44 1191.12 1315.44 1191.12 1259.94 1346.52 c 1,11,-1
    3.97 + 1364.28 1346.52 l 1,12,13
    3.98 + 1550.76 820.38 1550.76 820.38 2050.26 545.1 c 1,14,15
    3.99 + 1550.76 272.04 1550.76 272.04 1364.28 -256.32 c 1,16,-1
   3.100 + 1259.94 -256.32 l 1,17,18
   3.101 + 1311 -109.8 1311 -109.8 1419.78 70.0195 c 1,19,-1
   3.102 + 205.44 70.0195 l 2,20,21
   3.103 + 181.021 70.0195 181.021 70.0195 167.7 71.1299 c 128,-1,22
   3.104 + 154.38 72.2393 154.38 72.2393 141.061 83.3398 c 128,-1,23
   3.105 + 127.74 94.4395 127.74 94.4395 127.74 114.42 c 128,-1,24
   3.106 + 127.74 134.399 127.74 134.399 139.95 145.5 c 128,-1,25
   3.107 + 152.16 156.6 152.16 156.6 165.48 157.71 c 128,-1,26
   3.108 + 178.8 158.819 178.8 158.819 205.44 158.819 c 2,27,-1
   3.109 + 1439.76 158.819 l 2,28,29
   3.110 + 1470.84 158.819 1470.84 158.819 1479.72 162.149 c 128,-1,30
   3.111 + 1488.6 165.479 1488.6 165.479 1501.92 183.239 c 0,31,32
   3.112 + 1668.42 383.04 1668.42 383.04 1843.8 500.7 c 1,33,-1
   3.113 + 205.44 500.7 l 2,34,35
   3.114 + 176.58 500.7 176.58 500.7 164.37 501.81 c 128,-1,36
   3.115 + 152.16 502.92 152.16 502.92 139.95 514.02 c 128,-1,37
   3.116 + 127.74 525.12 127.74 525.12 127.74 545.1 c 0,38,39
   3.117 + 127.74 576.18 127.74 576.18 145.5 582.84 c 128,-1,40
   3.118 + 163.26 589.5 163.26 589.5 205.44 589.5 c 2,41,-1
   3.119 + 1843.8 589.5 l 1,42,43
   3.120 + 1663.98 711.6 1663.98 711.6 1501.92 909.18 c 0,44,45
   3.121 + 1488.6 924.72 1488.6 924.72 1479.72 928.05 c 128,-1,46
   3.122 + 1470.84 931.38 1470.84 931.38 1439.76 931.38 c 2,0,-1
   3.123 +EndSplineSet
   3.124 +EndChar
   3.125  EndChars
   3.126  EndSplineFont
     4.1 --- a/lib/fonts/IsabelleTextBold.sfd	Tue Dec 29 20:58:18 2015 +0100
     4.2 +++ b/lib/fonts/IsabelleTextBold.sfd	Tue Dec 29 21:51:58 2015 +0100
     4.3 @@ -20,7 +20,7 @@
     4.4  OS2_WeightWidthSlopeOnly: 0
     4.5  OS2_UseTypoMetrics: 1
     4.6  CreationTime: 1050374980
     4.7 -ModificationTime: 1451417467
     4.8 +ModificationTime: 1451421709
     4.9  PfmFamily: 17
    4.10  TTFWeight: 700
    4.11  TTFWidth: 5
    4.12 @@ -1678,10 +1678,10 @@
    4.13  DisplaySize: -96
    4.14  AntiAlias: 1
    4.15  FitToEm: 1
    4.16 -WinInfo: 8568 21 15
    4.17 +WinInfo: 8526 21 15
    4.18  BeginPrivate: 0
    4.19  EndPrivate
    4.20 -BeginChars: 1114115 1391
    4.21 +BeginChars: 1114115 1393
    4.22  
    4.23  StartChar: .notdef
    4.24  Encoding: 1114112 -1 0
    4.25 @@ -68539,5 +68539,121 @@
    4.26   4606.14 647.169 4606.14 647.169 4655.56 623.912 c 0,0,1
    4.27  EndSplineSet
    4.28  EndChar
    4.29 +
    4.30 +StartChar: uni21DA
    4.31 +Encoding: 8666 8666 1391
    4.32 +Width: 2174
    4.33 +VWidth: 2236
    4.34 +Flags: W
    4.35 +HStem: 45.0199 190.8<845.077 2084.29> 475.7 190.801<483.883 2084.96> 906.38 190.8<844.901 2084.29>
    4.36 +LayerCount: 2
    4.37 +Fore
    4.38 +SplineSet
    4.39 +1970.56 475.7 m 2,0,-1
    4.40 + 483.222 475.7 l 1,1,2
    4.41 + 602.389 374.701 602.389 374.701 713.152 239.802 c 0,3,4
    4.42 + 714.68 238.048 714.68 238.048 716.243 236.375 c 1,5,6
    4.43 + 724.064 235.82 724.064 235.82 736.24 235.82 c 2,7,-1
    4.44 + 1968.34 235.82 l 2,8,9
    4.45 + 1991.18 235.82 1991.18 235.82 2012.2 231.509 c 128,-1,10
    4.46 + 2033.23 227.199 2033.23 227.199 2053.86 217.305 c 128,-1,11
    4.47 + 2074.48 207.41 2074.48 207.41 2086.87 187.62 c 128,-1,12
    4.48 + 2099.26 167.831 2099.26 167.831 2099.26 140.42 c 0,13,14
    4.49 + 2099.26 96.5498 2099.26 96.5498 2067.59 70.1621 c 0,15,16
    4.50 + 2041.9 48.752 2041.9 48.752 2012.54 46.3066 c 0,17,18
    4.51 + 1997.1 45.0195 1997.1 45.0195 1970.56 45.0195 c 2,19,-1
    4.52 + 845.077 45.0195 l 1,20,21
    4.53 + 919.665 -88.791 919.665 -88.791 964.088 -213.167 c 2,22,-1
    4.54 + 988.429 -281.32 l 1,23,-1
    4.55 + 775.688 -281.32 l 1,24,-1
    4.56 + 763.65 -247.357 l 2,25,26
    4.57 + 583.658 260.503 583.658 260.503 101.124 526.434 c 2,27,-1
    4.58 + 19.749 571.281 l 1,28,-1
    4.59 + 101.277 615.85 l 2,29,30
    4.60 + 583.643 879.545 583.643 879.545 763.627 1389.49 c 2,31,-1
    4.61 + 775.636 1423.52 l 1,32,-1
    4.62 + 987.84 1423.52 l 1,33,-1
    4.63 + 964.219 1355.74 l 2,34,35
    4.64 + 922.776 1236.82 922.776 1236.82 844.901 1097.18 c 1,36,-1
    4.65 + 1970.56 1097.18 l 2,37,38
    4.66 + 1997.1 1097.18 1997.1 1097.18 2012.53 1095.89 c 0,39,40
    4.67 + 2041.9 1093.45 2041.9 1093.45 2067.59 1072.04 c 0,41,42
    4.68 + 2099.26 1045.65 2099.26 1045.65 2099.26 1001.78 c 0,43,44
    4.69 + 2099.26 974.743 2099.26 974.743 2086.77 955.016 c 128,-1,45
    4.70 + 2074.29 935.289 2074.29 935.289 2053.69 925.288 c 128,-1,46
    4.71 + 2033.09 915.288 2033.09 915.288 2011.96 910.834 c 128,-1,47
    4.72 + 1990.83 906.38 1990.83 906.38 1968.34 906.38 c 2,48,-1
    4.73 + 736.24 906.38 l 2,49,50
    4.74 + 725.34 906.38 725.34 906.38 717.649 905.919 c 1,51,52
    4.75 + 716.105 903.994 716.105 903.994 714.88 902.36 c 2,53,-1
    4.76 + 714.095 901.314 l 1,54,-1
    4.77 + 713.259 900.311 l 2,55,56
    4.78 + 600.95 765.537 600.95 765.537 483.883 666.5 c 1,57,-1
    4.79 + 1970.56 666.5 l 2,58,59
    4.80 + 1997.1 666.5 1997.1 666.5 2012.54 665.214 c 0,60,61
    4.81 + 2041.9 662.766 2041.9 662.766 2067.59 641.36 c 0,62,63
    4.82 + 2099.26 614.972 2099.26 614.972 2099.26 571.1 c 0,64,65
    4.83 + 2099.26 528.557 2099.26 528.557 2070.36 502.282 c 0,66,67
    4.84 + 2045.33 479.535 2045.33 479.535 2014.76 476.986 c 0,68,69
    4.85 + 1999.32 475.7 1999.32 475.7 1970.56 475.7 c 2,0,-1
    4.86 +EndSplineSet
    4.87 +EndChar
    4.88 +
    4.89 +StartChar: uni21DB
    4.90 +Encoding: 8667 8667 1392
    4.91 +Width: 2179
    4.92 +VWidth: 2236
    4.93 +Flags: W
    4.94 +HStem: 45.0199 190.8<91.0375 1331.1> 475.7 190.801<90.4486 1692.12> 906.38 190.8<91.0367 1330.92>
    4.95 +LayerCount: 2
    4.96 +Fore
    4.97 +SplineSet
    4.98 +1439.76 906.38 m 2,0,-1
    4.99 + 205.44 906.38 l 2,1,2
   4.100 + 178.899 906.38 178.899 906.38 163.464 907.666 c 0,3,4
   4.101 + 134.098 910.114 134.098 910.114 108.411 931.521 c 0,5,6
   4.102 + 76.7402 957.914 76.7402 957.914 76.7402 1001.78 c 0,7,8
   4.103 + 76.7402 1044.32 76.7402 1044.32 105.643 1070.6 c 0,9,10
   4.104 + 130.668 1093.35 130.668 1093.35 161.244 1095.89 c 0,11,12
   4.105 + 176.679 1097.18 176.679 1097.18 205.44 1097.18 c 2,13,-1
   4.106 + 1330.92 1097.18 l 1,14,15
   4.107 + 1256.32 1231 1256.32 1231 1211.91 1355.37 c 2,16,-1
   4.108 + 1187.57 1423.52 l 1,17,-1
   4.109 + 1400.31 1423.52 l 1,18,-1
   4.110 + 1412.35 1389.56 l 2,19,20
   4.111 + 1592.38 881.696 1592.38 881.696 2074.88 615.766 c 2,21,-1
   4.112 + 2156.25 570.919 l 1,22,-1
   4.113 + 2074.72 526.35 l 2,23,24
   4.114 + 1592.31 262.63 1592.31 262.63 1412.37 -247.294 c 2,25,-1
   4.115 + 1400.36 -281.32 l 1,26,-1
   4.116 + 1188.16 -281.32 l 1,27,-1
   4.117 + 1211.78 -213.537 l 2,28,29
   4.118 + 1253.22 -94.623 1253.22 -94.623 1331.1 45.0195 c 1,30,-1
   4.119 + 205.44 45.0195 l 2,31,32
   4.120 + 178.9 45.0195 178.9 45.0195 163.467 46.3066 c 0,33,34
   4.121 + 134.099 48.752 134.099 48.752 108.412 70.1602 c 0,35,36
   4.122 + 76.7402 96.5518 76.7402 96.5518 76.7402 140.42 c 0,37,38
   4.123 + 76.7402 182.96 76.7402 182.96 105.644 209.238 c 0,39,40
   4.124 + 130.668 231.985 130.668 231.985 161.247 234.534 c 0,41,42
   4.125 + 176.68 235.82 176.68 235.82 205.44 235.82 c 2,43,-1
   4.126 + 1439.76 235.82 l 2,44,45
   4.127 + 1450.66 235.82 1450.66 235.82 1458.35 236.281 c 1,46,47
   4.128 + 1459.9 238.207 1459.9 238.207 1461.12 239.84 c 2,48,-1
   4.129 + 1461.9 240.885 l 1,49,-1
   4.130 + 1462.74 241.889 l 2,50,51
   4.131 + 1575.02 376.632 1575.02 376.632 1692.12 475.7 c 1,52,-1
   4.132 + 205.44 475.7 l 2,53,54
   4.133 + 174.264 475.7 174.264 475.7 159.751 477.02 c 0,55,56
   4.134 + 130.509 479.679 130.509 479.679 105.644 502.282 c 0,57,58
   4.135 + 76.7402 528.558 76.7402 528.558 76.7402 571.1 c 0,59,60
   4.136 + 76.7402 597.362 76.7402 597.362 88.1611 621.725 c 128,-1,61
   4.137 + 99.582 646.089 99.582 646.089 127.592 656.593 c 0,62,63
   4.138 + 154.011 666.5 154.011 666.5 205.44 666.5 c 2,64,-1
   4.139 + 1692.78 666.5 l 1,65,66
   4.140 + 1573.58 767.53 1573.58 767.53 1462.84 902.402 c 0,67,68
   4.141 + 1461.32 904.153 1461.32 904.153 1459.76 905.825 c 1,69,70
   4.142 + 1451.94 906.38 1451.94 906.38 1439.76 906.38 c 2,0,-1
   4.143 +EndSplineSet
   4.144 +EndChar
   4.145  EndChars
   4.146  EndSplineFont
     5.1 --- a/lib/texinputs/isabellesym.sty	Tue Dec 29 20:58:18 2015 +0100
     5.2 +++ b/lib/texinputs/isabellesym.sty	Tue Dec 29 21:51:58 2015 +0100
     5.3 @@ -166,8 +166,10 @@
     5.4  \newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}}  %requires amsmath
     5.5  \newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
     5.6  \newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
     5.7 +\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}}  %requires amssymb
     5.8  \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
     5.9  \newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
    5.10 +\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}}  %requires amssymb
    5.11  \newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
    5.12  \newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
    5.13  \newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}