# HG changeset patch # User wenzelm # Date 1451422318 -3600 # Node ID 37a0cbee00c20fe3dac8573ba75620648dd30aa7 # Parent 2548e7cc86fbf3e857bcd51bfbf2c9fda4aceedf more arrow symbols; diff -r 2548e7cc86fb -r 37a0cbee00c2 NEWS --- 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: - - \ - \ - \ - \ - \ - \ - \ - \ +* Support for more arrow symbols, with rendering in LaTeX and +Isabelle fonts: \ \ \ \ \ \ *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 2548e7cc86fb -r 37a0cbee00c2 etc/symbols --- 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 @@ \ code: 0x0021e2 group: arrow abbrev: .> abbrev: ----> \ code: 0x0021d0 group: arrow abbrev: <. \ code: 0x0027f8 group: arrow abbrev: <. +\ code: 0x0021da group: arrow abbrev: <. \ code: 0x0021d2 group: arrow abbrev: .> abbrev: => \ code: 0x0027f9 group: arrow abbrev: .> abbrev: ==> +\ code: 0x0021db group: arrow abbrev: .> \ code: 0x002194 group: arrow abbrev: <> abbrev: <-> \ code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <--> \ code: 0x0021d4 group: arrow abbrev: <> diff -r 2548e7cc86fb -r 37a0cbee00c2 lib/fonts/IsabelleText.sfd --- 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 diff -r 2548e7cc86fb -r 37a0cbee00c2 lib/fonts/IsabelleTextBold.sfd --- 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 diff -r 2548e7cc86fb -r 37a0cbee00c2 lib/texinputs/isabellesym.sty --- 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}}