--- a/NEWS Tue Dec 29 20:58:18 2015 +0100
+++ b/NEWS Tue Dec 29 21:51:58 2015 +0100
@@ -31,17 +31,8 @@
remains available under print mode "ASCII", but less important syntax
has been removed (see below).
-* Support for arrows of various lengths, with rendering in LaTeX and
-Isabelle fonts:
-
- \<leftarrow>
- \<longleftarrow>
- \<longlongleftarrow>
- \<longlonglongleftarrow>
- \<rightarrow>
- \<longrightarrow>
- \<longlongrightarrow>
- \<longlonglongrightarrow>
+* Support for more arrow symbols, with rendering in LaTeX and
+Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/etc/symbols Tue Dec 29 20:58:18 2015 +0100
+++ b/etc/symbols Tue Dec 29 21:51:58 2015 +0100
@@ -164,8 +164,10 @@
\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .> abbrev: ---->
\<Leftarrow> code: 0x0021d0 group: arrow abbrev: <.
\<Longleftarrow> code: 0x0027f8 group: arrow abbrev: <.
+\<Lleftarrow> code: 0x0021da group: arrow abbrev: <.
\<Rightarrow> code: 0x0021d2 group: arrow abbrev: .> abbrev: =>
\<Longrightarrow> code: 0x0027f9 group: arrow abbrev: .> abbrev: ==>
+\<Rrightarrow> code: 0x0021db group: arrow abbrev: .>
\<leftrightarrow> code: 0x002194 group: arrow abbrev: <> abbrev: <->
\<longleftrightarrow> code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <-->
\<Leftrightarrow> code: 0x0021d4 group: arrow abbrev: <>
--- a/lib/fonts/IsabelleText.sfd Tue Dec 29 20:58:18 2015 +0100
+++ b/lib/fonts/IsabelleText.sfd Tue Dec 29 21:51:58 2015 +0100
@@ -19,7 +19,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1451417325
+ModificationTime: 1451421536
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2241,12 +2241,12 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 10278 18 16
+WinInfo: 8532 18 16
BeginPrivate: 0
EndPrivate
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
-BeginChars: 1114189 1399
-
+BeginChars: 1114189 1401
+
StartChar: u10000
Encoding: 65536 65536 0
AltUni2: 010000.ffffffff.0
@@ -62245,5 +62245,98 @@
2694 511.5 l 6,0,-1
EndSplineSet
EndChar
+
+StartChar: uni21DA
+Encoding: 8666 8666 1399
+Width: 2174
+VWidth: 2210
+Flags: W
+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>
+LayerCount: 2
+Fore
+SplineSet
+1970.56 500.7 m 2,0,-1
+ 332.2 500.7 l 1,1,2
+ 512.02 378.6 512.02 378.6 674.08 181.02 c 0,3,4
+ 687.4 165.479 687.4 165.479 696.28 162.149 c 128,-1,5
+ 705.16 158.819 705.16 158.819 736.24 158.819 c 2,6,-1
+ 1968.34 158.819 l 2,7,8
+ 2048.26 158.819 2048.26 158.819 2048.26 114.42 c 0,9,10
+ 2048.26 94.4395 2048.26 94.4395 2034.94 83.3398 c 128,-1,11
+ 2021.62 72.2393 2021.62 72.2393 2008.3 71.1299 c 128,-1,12
+ 1994.98 70.0195 1994.98 70.0195 1970.56 70.0195 c 2,13,-1
+ 756.22 70.0195 l 1,14,15
+ 860.56 -100.92 860.56 -100.92 916.06 -256.32 c 1,16,-1
+ 811.72 -256.32 l 1,17,18
+ 625.24 269.82 625.24 269.82 125.74 545.1 c 1,19,20
+ 625.24 818.16 625.24 818.16 811.72 1346.52 c 1,21,-1
+ 916.06 1346.52 l 1,22,23
+ 865 1200 865 1200 756.22 1020.18 c 1,24,-1
+ 1970.56 1020.18 l 2,25,26
+ 1994.98 1020.18 1994.98 1020.18 2008.3 1019.07 c 128,-1,27
+ 2021.62 1017.96 2021.62 1017.96 2034.94 1006.86 c 128,-1,28
+ 2048.26 995.76 2048.26 995.76 2048.26 975.78 c 0,29,30
+ 2048.26 931.38 2048.26 931.38 1968.34 931.38 c 2,31,-1
+ 736.24 931.38 l 2,32,33
+ 705.16 931.38 705.16 931.38 696.28 928.05 c 128,-1,34
+ 687.4 924.72 687.4 924.72 674.08 906.96 c 0,35,36
+ 507.58 707.16 507.58 707.16 332.2 589.5 c 1,37,-1
+ 1970.56 589.5 l 2,38,39
+ 1994.98 589.5 1994.98 589.5 2008.3 588.39 c 128,-1,40
+ 2021.62 587.28 2021.62 587.28 2034.94 576.18 c 128,-1,41
+ 2048.26 565.08 2048.26 565.08 2048.26 545.1 c 128,-1,42
+ 2048.26 525.12 2048.26 525.12 2036.05 514.02 c 128,-1,43
+ 2023.84 502.92 2023.84 502.92 2010.52 501.81 c 128,-1,44
+ 1997.2 500.7 1997.2 500.7 1970.56 500.7 c 2,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni21DB
+Encoding: 8667 8667 1400
+Width: 2179
+VWidth: 2210
+Flags: W
+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>
+LayerCount: 2
+Fore
+SplineSet
+1439.76 931.38 m 2,0,-1
+ 205.44 931.38 l 2,1,2
+ 181.021 931.38 181.021 931.38 167.7 932.49 c 128,-1,3
+ 154.38 933.6 154.38 933.6 141.061 944.7 c 128,-1,4
+ 127.74 955.8 127.74 955.8 127.74 975.78 c 128,-1,5
+ 127.74 995.76 127.74 995.76 139.95 1006.86 c 128,-1,6
+ 152.16 1017.96 152.16 1017.96 165.48 1019.07 c 128,-1,7
+ 178.8 1020.18 178.8 1020.18 205.44 1020.18 c 2,8,-1
+ 1419.78 1020.18 l 1,9,10
+ 1315.44 1191.12 1315.44 1191.12 1259.94 1346.52 c 1,11,-1
+ 1364.28 1346.52 l 1,12,13
+ 1550.76 820.38 1550.76 820.38 2050.26 545.1 c 1,14,15
+ 1550.76 272.04 1550.76 272.04 1364.28 -256.32 c 1,16,-1
+ 1259.94 -256.32 l 1,17,18
+ 1311 -109.8 1311 -109.8 1419.78 70.0195 c 1,19,-1
+ 205.44 70.0195 l 2,20,21
+ 181.021 70.0195 181.021 70.0195 167.7 71.1299 c 128,-1,22
+ 154.38 72.2393 154.38 72.2393 141.061 83.3398 c 128,-1,23
+ 127.74 94.4395 127.74 94.4395 127.74 114.42 c 128,-1,24
+ 127.74 134.399 127.74 134.399 139.95 145.5 c 128,-1,25
+ 152.16 156.6 152.16 156.6 165.48 157.71 c 128,-1,26
+ 178.8 158.819 178.8 158.819 205.44 158.819 c 2,27,-1
+ 1439.76 158.819 l 2,28,29
+ 1470.84 158.819 1470.84 158.819 1479.72 162.149 c 128,-1,30
+ 1488.6 165.479 1488.6 165.479 1501.92 183.239 c 0,31,32
+ 1668.42 383.04 1668.42 383.04 1843.8 500.7 c 1,33,-1
+ 205.44 500.7 l 2,34,35
+ 176.58 500.7 176.58 500.7 164.37 501.81 c 128,-1,36
+ 152.16 502.92 152.16 502.92 139.95 514.02 c 128,-1,37
+ 127.74 525.12 127.74 525.12 127.74 545.1 c 0,38,39
+ 127.74 576.18 127.74 576.18 145.5 582.84 c 128,-1,40
+ 163.26 589.5 163.26 589.5 205.44 589.5 c 2,41,-1
+ 1843.8 589.5 l 1,42,43
+ 1663.98 711.6 1663.98 711.6 1501.92 909.18 c 0,44,45
+ 1488.6 924.72 1488.6 924.72 1479.72 928.05 c 128,-1,46
+ 1470.84 931.38 1470.84 931.38 1439.76 931.38 c 2,0,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/lib/fonts/IsabelleTextBold.sfd Tue Dec 29 20:58:18 2015 +0100
+++ b/lib/fonts/IsabelleTextBold.sfd Tue Dec 29 21:51:58 2015 +0100
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1451417467
+ModificationTime: 1451421709
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1678,10 +1678,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 8568 21 15
+WinInfo: 8526 21 15
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1391
+BeginChars: 1114115 1393
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -68539,5 +68539,121 @@
4606.14 647.169 4606.14 647.169 4655.56 623.912 c 0,0,1
EndSplineSet
EndChar
+
+StartChar: uni21DA
+Encoding: 8666 8666 1391
+Width: 2174
+VWidth: 2236
+Flags: W
+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>
+LayerCount: 2
+Fore
+SplineSet
+1970.56 475.7 m 2,0,-1
+ 483.222 475.7 l 1,1,2
+ 602.389 374.701 602.389 374.701 713.152 239.802 c 0,3,4
+ 714.68 238.048 714.68 238.048 716.243 236.375 c 1,5,6
+ 724.064 235.82 724.064 235.82 736.24 235.82 c 2,7,-1
+ 1968.34 235.82 l 2,8,9
+ 1991.18 235.82 1991.18 235.82 2012.2 231.509 c 128,-1,10
+ 2033.23 227.199 2033.23 227.199 2053.86 217.305 c 128,-1,11
+ 2074.48 207.41 2074.48 207.41 2086.87 187.62 c 128,-1,12
+ 2099.26 167.831 2099.26 167.831 2099.26 140.42 c 0,13,14
+ 2099.26 96.5498 2099.26 96.5498 2067.59 70.1621 c 0,15,16
+ 2041.9 48.752 2041.9 48.752 2012.54 46.3066 c 0,17,18
+ 1997.1 45.0195 1997.1 45.0195 1970.56 45.0195 c 2,19,-1
+ 845.077 45.0195 l 1,20,21
+ 919.665 -88.791 919.665 -88.791 964.088 -213.167 c 2,22,-1
+ 988.429 -281.32 l 1,23,-1
+ 775.688 -281.32 l 1,24,-1
+ 763.65 -247.357 l 2,25,26
+ 583.658 260.503 583.658 260.503 101.124 526.434 c 2,27,-1
+ 19.749 571.281 l 1,28,-1
+ 101.277 615.85 l 2,29,30
+ 583.643 879.545 583.643 879.545 763.627 1389.49 c 2,31,-1
+ 775.636 1423.52 l 1,32,-1
+ 987.84 1423.52 l 1,33,-1
+ 964.219 1355.74 l 2,34,35
+ 922.776 1236.82 922.776 1236.82 844.901 1097.18 c 1,36,-1
+ 1970.56 1097.18 l 2,37,38
+ 1997.1 1097.18 1997.1 1097.18 2012.53 1095.89 c 0,39,40
+ 2041.9 1093.45 2041.9 1093.45 2067.59 1072.04 c 0,41,42
+ 2099.26 1045.65 2099.26 1045.65 2099.26 1001.78 c 0,43,44
+ 2099.26 974.743 2099.26 974.743 2086.77 955.016 c 128,-1,45
+ 2074.29 935.289 2074.29 935.289 2053.69 925.288 c 128,-1,46
+ 2033.09 915.288 2033.09 915.288 2011.96 910.834 c 128,-1,47
+ 1990.83 906.38 1990.83 906.38 1968.34 906.38 c 2,48,-1
+ 736.24 906.38 l 2,49,50
+ 725.34 906.38 725.34 906.38 717.649 905.919 c 1,51,52
+ 716.105 903.994 716.105 903.994 714.88 902.36 c 2,53,-1
+ 714.095 901.314 l 1,54,-1
+ 713.259 900.311 l 2,55,56
+ 600.95 765.537 600.95 765.537 483.883 666.5 c 1,57,-1
+ 1970.56 666.5 l 2,58,59
+ 1997.1 666.5 1997.1 666.5 2012.54 665.214 c 0,60,61
+ 2041.9 662.766 2041.9 662.766 2067.59 641.36 c 0,62,63
+ 2099.26 614.972 2099.26 614.972 2099.26 571.1 c 0,64,65
+ 2099.26 528.557 2099.26 528.557 2070.36 502.282 c 0,66,67
+ 2045.33 479.535 2045.33 479.535 2014.76 476.986 c 0,68,69
+ 1999.32 475.7 1999.32 475.7 1970.56 475.7 c 2,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni21DB
+Encoding: 8667 8667 1392
+Width: 2179
+VWidth: 2236
+Flags: W
+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>
+LayerCount: 2
+Fore
+SplineSet
+1439.76 906.38 m 2,0,-1
+ 205.44 906.38 l 2,1,2
+ 178.899 906.38 178.899 906.38 163.464 907.666 c 0,3,4
+ 134.098 910.114 134.098 910.114 108.411 931.521 c 0,5,6
+ 76.7402 957.914 76.7402 957.914 76.7402 1001.78 c 0,7,8
+ 76.7402 1044.32 76.7402 1044.32 105.643 1070.6 c 0,9,10
+ 130.668 1093.35 130.668 1093.35 161.244 1095.89 c 0,11,12
+ 176.679 1097.18 176.679 1097.18 205.44 1097.18 c 2,13,-1
+ 1330.92 1097.18 l 1,14,15
+ 1256.32 1231 1256.32 1231 1211.91 1355.37 c 2,16,-1
+ 1187.57 1423.52 l 1,17,-1
+ 1400.31 1423.52 l 1,18,-1
+ 1412.35 1389.56 l 2,19,20
+ 1592.38 881.696 1592.38 881.696 2074.88 615.766 c 2,21,-1
+ 2156.25 570.919 l 1,22,-1
+ 2074.72 526.35 l 2,23,24
+ 1592.31 262.63 1592.31 262.63 1412.37 -247.294 c 2,25,-1
+ 1400.36 -281.32 l 1,26,-1
+ 1188.16 -281.32 l 1,27,-1
+ 1211.78 -213.537 l 2,28,29
+ 1253.22 -94.623 1253.22 -94.623 1331.1 45.0195 c 1,30,-1
+ 205.44 45.0195 l 2,31,32
+ 178.9 45.0195 178.9 45.0195 163.467 46.3066 c 0,33,34
+ 134.099 48.752 134.099 48.752 108.412 70.1602 c 0,35,36
+ 76.7402 96.5518 76.7402 96.5518 76.7402 140.42 c 0,37,38
+ 76.7402 182.96 76.7402 182.96 105.644 209.238 c 0,39,40
+ 130.668 231.985 130.668 231.985 161.247 234.534 c 0,41,42
+ 176.68 235.82 176.68 235.82 205.44 235.82 c 2,43,-1
+ 1439.76 235.82 l 2,44,45
+ 1450.66 235.82 1450.66 235.82 1458.35 236.281 c 1,46,47
+ 1459.9 238.207 1459.9 238.207 1461.12 239.84 c 2,48,-1
+ 1461.9 240.885 l 1,49,-1
+ 1462.74 241.889 l 2,50,51
+ 1575.02 376.632 1575.02 376.632 1692.12 475.7 c 1,52,-1
+ 205.44 475.7 l 2,53,54
+ 174.264 475.7 174.264 475.7 159.751 477.02 c 0,55,56
+ 130.509 479.679 130.509 479.679 105.644 502.282 c 0,57,58
+ 76.7402 528.558 76.7402 528.558 76.7402 571.1 c 0,59,60
+ 76.7402 597.362 76.7402 597.362 88.1611 621.725 c 128,-1,61
+ 99.582 646.089 99.582 646.089 127.592 656.593 c 0,62,63
+ 154.011 666.5 154.011 666.5 205.44 666.5 c 2,64,-1
+ 1692.78 666.5 l 1,65,66
+ 1573.58 767.53 1573.58 767.53 1462.84 902.402 c 0,67,68
+ 1461.32 904.153 1461.32 904.153 1459.76 905.825 c 1,69,70
+ 1451.94 906.38 1451.94 906.38 1439.76 906.38 c 2,0,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/lib/texinputs/isabellesym.sty Tue Dec 29 20:58:18 2015 +0100
+++ b/lib/texinputs/isabellesym.sty Tue Dec 29 21:51:58 2015 +0100
@@ -166,8 +166,10 @@
\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath
\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb
\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb
\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}