--- a/Admin/components/components.sha1 Wed Jul 17 16:32:06 2019 +0100
+++ b/Admin/components/components.sha1 Wed Jul 17 22:24:20 2019 +0200
@@ -87,6 +87,7 @@
dfcdf9a757b9dc36cee87f82533b43c58ba84abe isabelle_fonts-20190309.tar.gz
95e3acf038df7fdeeacd8b4769930e6f57bf3692 isabelle_fonts-20190406.tar.gz
dabcf5085d67c99159007007ff0e9bf775e423d1 isabelle_fonts-20190409.tar.gz
+76827987c70051719e117138858930d42041f57d isabelle_fonts-20190717.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
06ac8993b5bebd02c70f1bd18ce13075f01115f3 jdk-11.0.3+7.tar.gz
@@ -160,6 +161,7 @@
58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz
ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz
1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz
+b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Wed Jul 17 16:32:06 2019 +0100
+++ b/Admin/components/main Wed Jul 17 22:24:20 2019 +0200
@@ -4,9 +4,9 @@
csdp-6.x
cvc4-1.5-5
e-2.0-2
-isabelle_fonts-20190409
+isabelle_fonts-20190717
jdk-11.0.3+7
-jedit_build-20190508
+jedit_build-20190717
jfreechart-1.5.0
jortho-1.0-2
kodkodi-1.5.2-1
--- a/Admin/isabelle_fonts/IsabelleSymbols.sfd Wed Jul 17 16:32:06 2019 +0100
+++ b/Admin/isabelle_fonts/IsabelleSymbols.sfd Wed Jul 17 22:24:20 2019 +0200
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1544375065
+ModificationTime: 1563371335
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2242,11 +2242,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 0 32 8
+WinInfo: 10112 32 8
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 1411
+BeginChars: 1114189 1414
StartChar: u10000
Encoding: 65536 65536 0
@@ -16356,24 +16356,19 @@
StartChar: periodcentered
Encoding: 183 183 195
Width: 614
-VWidth: 2220
-Flags: W
-HStem: 437 235<214.472 402.688>
-VStem: 191 235<460.892 649.108>
-LayerCount: 2
-Fore
-SplineSet
-426 555 m 128,-1,1
- 426 507 426 507 391.5 472 c 128,-1,2
- 357 437 357 437 308.5 437 c 128,-1,3
- 260 437 260 437 225.5 472 c 128,-1,4
- 191 507 191 507 191 555 c 128,-1,5
- 191 603 191 603 225.5 638 c 128,-1,6
- 260 673 260 673 308.5 672.5 c 128,-1,7
- 357 672 357 672 391.5 637.5 c 128,-1,0
- 426 603 426 603 426 555 c 128,-1,1
-EndSplineSet
-Validated: 33
+VWidth: 2326
+Flags: W
+HStem: 415.188 375.624<115.193 498.807>
+VStem: 115.193 383.614<415.188 790.812>
+LayerCount: 2
+Fore
+SplineSet
+115.193359375 790.811523438 m 1,0,-1
+ 498.806640625 790.811523438 l 1,1,-1
+ 498.806640625 415.188476562 l 1,2,-1
+ 115.193359375 415.188476562 l 1,3,-1
+ 115.193359375 790.811523438 l 1,0,-1
+EndSplineSet
EndChar
StartChar: quotesinglbase
@@ -61633,5 +61628,128 @@
578 410 l 1,19,-1
EndSplineSet
EndChar
+
+StartChar: uni2AFF
+Encoding: 11007 11007 1411
+Width: 1151
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+350 1576 m 1,0,-1
+ 350 -466 l 1,1,-1
+ 788 -466 l 1,2,-1
+ 788 1576 l 1,3,-1
+ 350 1576 l 1,0,-1
+264 1670 m 1,4,-1
+ 880 1670 l 1,5,-1
+ 880 -558 l 1,6,-1
+ 264 -558 l 1,7,-1
+ 264 1670 l 1,4,-1
+EndSplineSet
+EndChar
+
+StartChar: uni27EA
+Encoding: 10218 10218 1412
+Width: 1161
+VWidth: 2220
+Flags: W
+VStem: 244 493
+LayerCount: 2
+Fore
+SplineSet
+726 1581 m 2,0,-1
+ 335 555 l 1,1,-1
+ 726 -471 l 2,2,3
+ 737 -498 737 -498 737 -511 c 0,4,5
+ 737 -529 737 -529 724 -542 c 128,-1,6
+ 711 -555 711 -555 693 -555 c 0,7,8
+ 684 -555 684 -555 677 -552.5 c 128,-1,9
+ 670 -550 670 -550 665.5 -545.5 c 128,-1,10
+ 661 -541 661 -541 657 -535 c 128,-1,11
+ 653 -529 653 -529 650 -521.5 c 128,-1,12
+ 647 -514 647 -514 644 -506 c 2,13,-1
+ 255 515 l 2,14,15
+ 244 542 244 542 244 555 c 128,-1,16
+ 244 568 244 568 255 595 c 2,17,-1
+ 646 1621 l 2,18,19
+ 651 1636 651 1636 655.5 1644 c 128,-1,20
+ 660 1652 660 1652 669.5 1658.5 c 128,-1,21
+ 679 1665 679 1665 693 1665 c 0,22,23
+ 711 1665 711 1665 724 1652 c 128,-1,24
+ 737 1639 737 1639 737 1621 c 0,25,26
+ 737 1608 737 1608 726 1581 c 2,0,-1
+1026 1581 m 2,27,-1
+ 635 555 l 1,28,-1
+ 1026 -471 l 2,29,30
+ 1037 -498 1037 -498 1037 -511 c 0,31,32
+ 1037 -529 1037 -529 1024 -542 c 128,-1,33
+ 1011 -555 1011 -555 993 -555 c 0,34,35
+ 984 -555 984 -555 977 -552.5 c 128,-1,36
+ 970 -550 970 -550 965.5 -545.5 c 128,-1,37
+ 961 -541 961 -541 957 -535 c 128,-1,38
+ 953 -529 953 -529 950 -521.5 c 128,-1,39
+ 947 -514 947 -514 944 -506 c 2,40,-1
+ 555 515 l 2,41,42
+ 544 542 544 542 544 555 c 128,-1,43
+ 544 568 544 568 555 595 c 2,44,-1
+ 946 1621 l 2,45,46
+ 951 1636 951 1636 955.5 1644 c 128,-1,47
+ 960 1652 960 1652 969.5 1658.5 c 128,-1,48
+ 979 1665 979 1665 993 1665 c 0,49,50
+ 1011 1665 1011 1665 1024 1652 c 128,-1,51
+ 1037 1639 1037 1639 1037 1621 c 0,52,53
+ 1037 1608 1037 1608 1026 1581 c 2,27,-1
+EndSplineSet
+EndChar
+
+StartChar: uni27EB
+Encoding: 10219 10219 1413
+Width: 1061
+VWidth: 2220
+Flags: W
+HStem: -555 47<157 183> 1621 44<157 184>
+VStem: 124 493
+LayerCount: 2
+Fore
+SplineSet
+606 515 m 2,0,-1
+ 215 -511 l 2,1,2
+ 199 -555 199 -555 169 -555 c 0,3,4
+ 151 -555 151 -555 137.5 -541.5 c 128,-1,5
+ 124 -528 124 -528 124 -511 c 0,6,7
+ 124 -498 124 -498 135 -471 c 2,8,-1
+ 526 555 l 1,9,-1
+ 135 1581 l 2,10,11
+ 124 1608 124 1608 124 1621 c 0,12,13
+ 124 1639 124 1639 137.5 1652 c 128,-1,14
+ 151 1665 151 1665 169 1665 c 0,15,16
+ 180 1665 180 1665 187.5 1663 c 128,-1,17
+ 195 1661 195 1661 202 1649.5 c 128,-1,18
+ 209 1638 209 1638 210 1636 c 128,-1,19
+ 211 1634 211 1634 218 1616 c 2,20,-1
+ 606 595 l 2,21,22
+ 617 568 617 568 617 555 c 128,-1,23
+ 617 542 617 542 606 515 c 2,0,-1
+906 515 m 2,24,-1
+ 515 -511 l 2,25,26
+ 499 -555 499 -555 469 -555 c 0,27,28
+ 451 -555 451 -555 437.5 -541.5 c 128,-1,29
+ 424 -528 424 -528 424 -511 c 0,30,31
+ 424 -498 424 -498 435 -471 c 2,32,-1
+ 826 555 l 1,33,-1
+ 435 1581 l 2,34,35
+ 424 1608 424 1608 424 1621 c 0,36,37
+ 424 1639 424 1639 437.5 1652 c 128,-1,38
+ 451 1665 451 1665 469 1665 c 0,39,40
+ 480 1665 480 1665 487.5 1663 c 128,-1,41
+ 495 1661 495 1661 502 1649.5 c 128,-1,42
+ 509 1638 509 1638 510 1636 c 128,-1,43
+ 511 1634 511 1634 518 1616 c 2,44,-1
+ 906 595 l 2,45,46
+ 917 568 917 568 917 555 c 128,-1,47
+ 917 542 917 542 906 515 c 2,24,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Wed Jul 17 16:32:06 2019 +0100
+++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Wed Jul 17 22:24:20 2019 +0200
@@ -21,7 +21,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1544375307
+ModificationTime: 1563372497
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1679,10 +1679,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 0 32 8
+WinInfo: 10176 32 8
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1403
+BeginChars: 1114115 1406
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -13029,20 +13029,24 @@
StartChar: periodcentered
Encoding: 183 183 125
Width: 614
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-427.5 436 m 128,-1,1
- 378 386 378 386 308.5 386 c 128,-1,2
- 239 386 239 386 189.5 436 c 128,-1,3
- 140 486 140 486 140 555 c 128,-1,4
- 140 624 140 624 189 674 c 128,-1,5
- 238 724 238 724 307 724 c 1,6,-1
- 343 723 l 2,7,8
- 378 723 378 723 427.5 673.5 c 128,-1,9
- 477 624 477 624 477 555 c 128,-1,0
- 477 486 477 486 427.5 436 c 128,-1,1
+VWidth: 2326
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+115.193359375 841.811523438 m 1,0,-1
+ 498.806640625 841.811523438 l 1,1,-1
+ 549.806640625 841.811523438 l 1,2,-1
+ 549.806640625 790.811523438 l 1,3,-1
+ 549.806640625 415.188476562 l 1,4,-1
+ 549.806640625 364.188476562 l 1,5,-1
+ 498.806640625 364.188476562 l 1,6,-1
+ 115.193359375 364.188476562 l 1,7,-1
+ 64.193359375 364.188476562 l 1,8,-1
+ 64.193359375 415.188476562 l 1,9,-1
+ 64.193359375 790.811523438 l 1,10,-1
+ 64.193359375 841.811523438 l 1,11,-1
+ 115.193359375 841.811523438 l 1,0,-1
EndSplineSet
EndChar
@@ -69151,5 +69155,194 @@
547 440 l 1,19,-1
EndSplineSet
EndChar
+
+StartChar: uni2AFF
+Encoding: 11007 11007 1403
+Width: 1151
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+401 1525 m 1,0,-1
+ 401 -415 l 1,1,-1
+ 737 -415 l 1,2,-1
+ 737 1525 l 1,3,-1
+ 401 1525 l 1,0,-1
+264 1721 m 1,4,-1
+ 880 1721 l 1,5,-1
+ 931 1721 l 1,6,-1
+ 931 1670 l 1,7,-1
+ 931 -558 l 1,8,-1
+ 931 -609 l 1,9,-1
+ 880 -609 l 1,10,-1
+ 264 -609 l 1,11,-1
+ 213 -609 l 1,12,-1
+ 213 -558 l 1,13,-1
+ 213 1670 l 1,14,-1
+ 213 1721 l 1,15,-1
+ 264 1721 l 1,4,-1
+EndSplineSet
+EndChar
+
+StartChar: uni27EA
+Encoding: 10218 10218 1404
+Width: 1161
+VWidth: 2220
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+773.433067855 1562.25171141 m 2
+ 389.577883489 555 l 1
+ 773.433067855 -452.251711406 l 2
+ 781.390968826 -472.014126234 781.390968826 -472.014126234 784.695484413 -483.995108037 c 0
+ 788 -495.97608984 788 -495.97608984 788 -511 c 0
+ 788 -550.124891681 788 -550.124891681 760.062445841 -578.062445841 c 0
+ 732.124891681 -606 732.124891681 -606 693 -606 c 0
+ 690.966017759 -606 690.966017759 -606 688.963489691 -605.928643068 c 0
+ 686.960961624 -605.857286137 686.960961624 -605.857286137 684.892393771 -605.709011758 c 0
+ 682.823825917 -605.560737379 682.823825917 -605.560737379 680.76747727 -605.324534758 c 0
+ 678.711128623 -605.088332136 678.711128623 -605.088332136 676.625730612 -604.767155106 c 0
+ 674.540332601 -604.445978076 674.540332601 -604.445978076 672.44417047 -604.01973387 c 0
+ 670.348008338 -603.593489663 670.348008338 -603.593489663 668.259787265 -603.074214086 c 0
+ 666.171566192 -602.554938509 666.171566192 -602.554938509 664.049597672 -601.913456822 c 0
+ 661.927629152 -601.271975134 661.927629152 -601.271975134 659.846843753 -600.528837491 c 0
+ 654.406114092 -598.585719755 654.406114092 -598.585719755 649.309616546 -595.97667424 c 0
+ 644.213119 -593.367628724 644.213119 -593.367628724 639.0284107 -589.668111402 c 0
+ 633.8437024 -585.968594081 633.8437024 -585.968594081 629.437554159 -581.562445841 c 0
+ 621.366668313 -573.491559994 621.366668313 -573.491559994 614.565434989 -563.289710007 c 0
+ 611.010645977 -557.95752649 611.010645977 -557.95752649 608.043624405 -552.235368077 c 0
+ 605.076602833 -546.513209663 605.076602833 -546.513209663 602.647688765 -540.440924494 c 0
+ 601.07426099 -536.507355058 601.07426099 -536.507355058 599.445196471 -532.299218632 c 0
+ 597.816131951 -528.091082206 597.816131951 -528.091082206 596.294209878 -524.032623346 c 2
+ 207.565919702 496.254225678 l 2
+ 199.609686199 516.012499566 199.609686199 516.012499566 196.304843099 527.994862915 c 0
+ 193 539.977226263 193 539.977226263 193 555 c 0
+ 193 565.225713049 193 565.225713049 195.245324552 576.018756482 c 0
+ 197.490649104 586.811799915 197.490649104 586.811799915 200.081716986 594.203054286 c 0
+ 202.672784867 601.594308656 202.672784867 601.594308656 207.566932145 613.748288594 c 2
+ 597.972039167 1638.18726508 l 2
+ 600.194483765 1644.75231063 600.194483765 1644.75231063 601.986957781 1649.47802294 c 0
+ 603.779431796 1654.20373526 603.779431796 1654.20373526 606.068369421 1659.21033763 c 0
+ 608.357307047 1664.21694 608.357307047 1664.21694 611.049647607 1669.00332322 c 0
+ 621.382343055 1687.37255957 621.382343055 1687.37255957 640.701120305 1700.59067032 c 0
+ 663.222448293 1716 663.222448293 1716 693 1716 c 0
+ 700.423944801 1716 700.423944801 1716 707.872943823 1714.76786733 c 0
+ 715.321942844 1713.53573466 715.321942844 1713.53573466 722.391875006 1711.16829501 c 0
+ 729.461807167 1708.80085536 729.461807167 1708.80085536 736.118390492 1705.41106402 c 0
+ 742.774973817 1702.02127269 742.774973817 1702.02127269 748.821381789 1697.6391873 c 0
+ 754.867789762 1693.25710192 754.867789762 1693.25710192 760.062445841 1688.06244584 c 0
+ 768.737564682 1679.387327 768.737564682 1679.387327 775.010481308 1668.56083179 c 0
+ 781.283397934 1657.73433659 781.283397934 1657.73433659 784.641698967 1645.54589151 c 0
+ 788 1633.35744643 788 1633.35744643 788 1621 c 0
+ 788 1610.77428695 788 1610.77428695 785.754675448 1599.98124352 c 0
+ 783.509350896 1589.18820008 783.509350896 1589.18820008 780.918283014 1581.79694571 c 0
+ 778.327215133 1574.40569134 778.327215133 1574.40569134 773.433067855 1562.25171141 c 2
+1073.43306785 1562.25171141 m 2
+ 689.577883489 555 l 1
+ 1073.43306785 -452.251711406 l 2
+ 1088 -488.426797886 1088 -488.426797886 1088 -511 c 0
+ 1088 -518.423944801 1088 -518.423944801 1086.76786733 -525.872943823 c 0
+ 1085.53573466 -533.321942844 1085.53573466 -533.321942844 1083.16829501 -540.391875006 c 0
+ 1080.80085536 -547.461807167 1080.80085536 -547.461807167 1077.41106402 -554.118390492 c 0
+ 1074.02127269 -560.774973817 1074.02127269 -560.774973817 1069.6391873 -566.821381789 c 0
+ 1065.25710192 -572.867789762 1065.25710192 -572.867789762 1060.06244584 -578.062445841 c 0
+ 1046.94472562 -591.180166062 1046.94472562 -591.180166062 1029.27411163 -598.590083031 c 0
+ 1011.60349764 -606 1011.60349764 -606 993 -606 c 0
+ 984.51752108 -606 984.51752108 -606 976.206536445 -604.701688042 c 0
+ 967.895551811 -603.403376083 967.895551811 -603.403376083 959.846843753 -600.528837491 c 0
+ 954.406114092 -598.585719755 954.406114092 -598.585719755 949.309616546 -595.97667424 c 0
+ 944.213119 -593.367628724 944.213119 -593.367628724 939.0284107 -589.668111402 c 0
+ 933.8437024 -585.968594081 933.8437024 -585.968594081 929.437554159 -581.562445841 c 0
+ 921.366668313 -573.491559994 921.366668313 -573.491559994 914.565434989 -563.289710007 c 0
+ 911.010645977 -557.95752649 911.010645977 -557.95752649 908.043624405 -552.235368077 c 0
+ 905.076602833 -546.513209663 905.076602833 -546.513209663 902.647688765 -540.440924494 c 0
+ 901.07426099 -536.507355058 901.07426099 -536.507355058 899.445196471 -532.299218632 c 0
+ 897.816131951 -528.091082206 897.816131951 -528.091082206 896.294209878 -524.032623346 c 2
+ 507.565919702 496.254225678 l 2
+ 499.609686199 516.012499566 499.609686199 516.012499566 496.304843099 527.994862915 c 0
+ 493 539.977226263 493 539.977226263 493 555 c 0
+ 493 562.810879998 493 562.810879998 494.055472434 570.258924161 c 0
+ 495.110944868 577.706968323 495.110944868 577.706968323 497.451348895 585.545645538 c 0
+ 499.791752921 593.384322753 499.791752921 593.384322753 501.859659434 599.04735873 c 0
+ 503.927565946 604.710394707 503.927565946 604.710394707 507.566932145 613.748288594 c 2
+ 897.972039167 1638.18726508 l 2
+ 901.32118185 1648.08054848 901.32118185 1648.08054848 904.224607807 1655.05605688 c 0
+ 907.128033763 1662.03156528 907.128033763 1662.03156528 911.049647607 1669.00332322 c 0
+ 921.382343055 1687.37255957 921.382343055 1687.37255957 940.701120305 1700.59067032 c 0
+ 963.222448293 1716 963.222448293 1716 993 1716 c 0
+ 1000.4239448 1716 1000.4239448 1716 1007.87294382 1714.76786733 c 0
+ 1015.32194284 1713.53573466 1015.32194284 1713.53573466 1022.39187501 1711.16829501 c 0
+ 1029.46180717 1708.80085536 1029.46180717 1708.80085536 1036.11839049 1705.41106402 c 0
+ 1042.77497382 1702.02127269 1042.77497382 1702.02127269 1048.82138179 1697.6391873 c 0
+ 1054.86778976 1693.25710192 1054.86778976 1693.25710192 1060.06244584 1688.06244584 c 0
+ 1073.18016606 1674.94472562 1073.18016606 1674.94472562 1080.59008303 1657.27411163 c 0
+ 1088 1639.60349764 1088 1639.60349764 1088 1621 c 0
+ 1088 1598.42679789 1088 1598.42679789 1073.43306785 1562.25171141 c 2
+EndSplineSet
+EndChar
+
+StartChar: uni27EB
+Encoding: 10219 10219 1405
+Width: 1061
+VWidth: 2220
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+653.433067855 496.251711406 m 2
+ 262.795873515 -528.796271696 l 2
+ 255.492538225 -548.880443742 255.492538225 -548.880443742 244.246012333 -565.137792244 c 0
+ 232.99948644 -581.395140747 232.99948644 -581.395140747 213.079715784 -593.697570373 c 0
+ 193.159945129 -606 193.159945129 -606 169 -606 c 0
+ 129.875108319 -606 129.875108319 -606 101.437554159 -577.562445841 c 0
+ 73 -549.124891681 73 -549.124891681 73 -511 c 0
+ 73 -488.426797886 73 -488.426797886 87.5669321452 -452.251711406 c 2
+ 471.422116511 555 l 1
+ 87.5669321452 1562.25171141 l 2
+ 73 1598.42679789 73 1598.42679789 73 1621 c 0
+ 73 1633.6040069 73 1633.6040069 76.5609657568 1646.01567027 c 0
+ 80.1219315135 1658.42733364 80.1219315135 1658.42733364 86.6484595992 1669.27291665 c 0
+ 93.1749876849 1680.11849966 93.1749876849 1680.11849966 102.12427396 1688.73633089 c 0
+ 115.390346368 1701.51106728 115.390346368 1701.51106728 132.945757373 1708.75553364 c 0
+ 150.501168378 1716 150.501168378 1716 169 1716 c 0
+ 186.683227377 1716 186.683227377 1716 200.640795179 1712.27798192 c 0
+ 227.920396727 1705.00342151 227.920396727 1705.00342151 245.564126336 1676.01729429 c 0
+ 253.667102023 1662.70526281 253.667102023 1662.70526281 255.615786741 1658.80789337 c 0
+ 257.674333935 1654.69079898 257.674333935 1654.69079898 265.603655969 1634.30111375 c 2
+ 653.444670969 613.719473764 l 2
+ 661.383463777 594.004511582 661.383463777 594.004511582 664.691731888 582.007697863 c 0
+ 668 570.010884144 668 570.010884144 668 555 c 0
+ 668 540.337813677 668 540.337813677 664.406510997 527.45834196 c 0
+ 660.813021994 514.578870243 660.813021994 514.578870243 653.433067855 496.251711406 c 2
+953.433067855 496.251711406 m 2
+ 562.795873515 -528.796271696 l 2
+ 551.145513147 -560.834762708 551.145513147 -560.834762708 527.661549555 -583.417381354 c 0
+ 504.177585963 -606 504.177585963 -606 469 -606 c 0
+ 429.875108319 -606 429.875108319 -606 401.437554159 -577.562445841 c 0
+ 373 -549.124891681 373 -549.124891681 373 -511 c 0
+ 373 -500.774286951 373 -500.774286951 375.245324552 -489.981243518 c 0
+ 377.490649104 -479.188200085 377.490649104 -479.188200085 380.081716986 -471.796945714 c 0
+ 382.672784867 -464.405691344 382.672784867 -464.405691344 387.566932145 -452.251711406 c 2
+ 771.422116511 555 l 1
+ 387.566932145 1562.25171141 l 2
+ 373 1598.42679789 373 1598.42679789 373 1621 c 0
+ 373 1639.9408395 373 1639.9408395 380.780095648 1657.80773058 c 0
+ 388.560191296 1675.67462166 388.560191296 1675.67462166 402.12427396 1688.73633089 c 0
+ 410.883148534 1697.1708027 410.883148534 1697.1708027 421.628761565 1703.27369144 c 0
+ 432.374374596 1709.37658019 432.374374596 1709.37658019 444.529941996 1712.68829009 c 0
+ 456.685509397 1716 456.685509397 1716 469 1716 c 0
+ 486.683227377 1716 486.683227377 1716 500.640795179 1712.27798192 c 0
+ 527.920396727 1705.00342151 527.920396727 1705.00342151 545.564126336 1676.01729429 c 0
+ 553.667102023 1662.70526281 553.667102023 1662.70526281 555.615786741 1658.80789337 c 0
+ 556.9883423 1656.06278225 556.9883423 1656.06278225 558.118524875 1653.46941152 c 0
+ 559.248707449 1650.87604078 559.248707449 1650.87604078 559.967222509 1649.02866899 c 0
+ 560.685737568 1647.18129719 560.685737568 1647.18129719 562.420306544 1642.60392319 c 0
+ 564.154875519 1638.02654919 564.154875519 1638.02654919 565.603655969 1634.30111375 c 2
+ 953.444670969 613.719473764 l 2
+ 968 577.573202114 968 577.573202114 968 555 c 0
+ 968 532.426797886 968 532.426797886 953.433067855 496.251711406 c 2
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/Admin/isabelle_fonts/README Wed Jul 17 16:32:06 2019 +0100
+++ b/Admin/isabelle_fonts/README Wed Jul 17 22:24:20 2019 +0200
@@ -4,11 +4,11 @@
The Isabelle fonts are subject to the same BSD-3-clause license as Isabelle.
TTF files are produced automatically from the Deja Vu font family with symbols
-from the IsabelleText font:
+from the IsabelleSymbols font (formerly IsabelleText):
isabelle build_fonts -d dejavu-fonts-ttf-2.37/ttf
-The IsabelleText template (see Admin/isabelle_fonts in the repository) has
+The IsabelleSymbols template (see Admin/isabelle_fonts in the repository) has
been assembled manually, by composing glyphs from Bluesky TeX fonts (scaled
222%) with some additions from DejaVu Sans Mono and DejaVu Sans. Some
additional symbols are from Symbola, see http://greekfonts.teilar.gr "In lieu
@@ -17,7 +17,7 @@
Makarius
- 10-Feb-2019
+ 17-Jul-2019
----------------------------------------------------------------------------
--- a/etc/symbols Wed Jul 17 16:32:06 2019 +0100
+++ b/etc/symbols Wed Jul 17 22:24:20 2019 +0200
@@ -198,6 +198,8 @@
\<Updown> code: 0x0021d5 group: arrow
\<langle> code: 0x0027e8 group: punctuation abbrev: <<
\<rangle> code: 0x0027e9 group: punctuation abbrev: >>
+\<llangle> code: 0x0027ea group: punctuation abbrev: <<
+\<rrangle> code: 0x0027eb group: punctuation abbrev: >>
\<lceil> code: 0x002308 group: punctuation abbrev: [.
\<rceil> code: 0x002309 group: punctuation abbrev: .]
\<lfloor> code: 0x00230a group: punctuation abbrev: [.
@@ -278,6 +280,7 @@
\<succeq> code: 0x00227d group: relation
\<parallel> code: 0x002225 group: punctuation abbrev: ||
\<bar> code: 0x0000a6 group: punctuation abbrev: ||
+\<bbar> code: 0x002aff group: punctuation abbrev: ||
\<plusminus> code: 0x0000b1 group: operator
\<minusplus> code: 0x002213 group: operator
\<times> code: 0x0000d7 group: operator abbrev: <*>
@@ -328,6 +331,7 @@
\<registered> code: 0x0000ae
\<hyphen> code: 0x002010 group: punctuation
\<inverse> code: 0x0000af group: operator
+\<sqdot> code: 0x0000b7 group: punctuation
\<onequarter> code: 0x0000bc group: digit
\<onehalf> code: 0x0000bd group: digit
\<threequarters> code: 0x0000be group: digit
--- a/lib/texinputs/isabelle.sty Wed Jul 17 16:32:06 2019 +0100
+++ b/lib/texinputs/isabelle.sty Wed Jul 17 22:24:20 2019 +0200
@@ -207,8 +207,6 @@
\def\isachartilde{\isamath{{}\sp{\sim}}}%
\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
-\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
-\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
}
\newcommand{\isabellestyleliteral}{%
--- a/lib/texinputs/isabellesym.sty Wed Jul 17 16:32:06 2019 +0100
+++ b/lib/texinputs/isabellesym.sty Wed Jul 17 22:24:20 2019 +0200
@@ -200,6 +200,8 @@
\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
\newcommand{\isasymlangle}{\isamath{\langle}}
\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}}
+\newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}}
\newcommand{\isasymlceil}{\isamath{\lceil}}
\newcommand{\isasymrceil}{\isamath{\rceil}}
\newcommand{\isasymlfloor}{\isamath{\lfloor}}
@@ -280,11 +282,13 @@
\newcommand{\isasymsucceq}{\isamath{\succeq}}
\newcommand{\isasymparallel}{\isamath{\parallel}}
\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}}
\newcommand{\isasymplusminus}{\isamath{\pm}}
\newcommand{\isasymminusplus}{\isamath{\mp}}
\newcommand{\isasymtimes}{\isamath{\times}}
\newcommand{\isasymdiv}{\isamath{\div}}
\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}} %requires amssymb
\newcommand{\isasymstar}{\isamath{\star}}
\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
\newcommand{\isasymcirc}{\isamath{\circ}}
--- a/src/Pure/Admin/build_fonts.scala Wed Jul 17 16:32:06 2019 +0100
+++ b/src/Pure/Admin/build_fonts.scala Wed Jul 17 22:24:20 2019 +0200
@@ -96,6 +96,8 @@
0x27e7, // right white square bracket
0x27e8, // left angle bracket
0x27e9, // right angle bracket
+ 0x27ea, // left double angle bracket
+ 0x27eb, // right double angle bracket
) ++
(0x27f0 to 0x27ff) ++ // Supplemental Arrows-A
(0x2900 to 0x297f) ++ // Supplemental Arrows-B
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/brackets Wed Jul 17 22:24:20 2019 +0200
@@ -0,0 +1,25 @@
+--- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2018-04-09 01:58:01.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2019-07-17 21:36:43.985183582 +0200
+@@ -1625,8 +1630,8 @@
+ }
+
+ // Scan backwards, trying to find a bracket
+- String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
+- String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄";
++ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
++ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
+ int count = 1;
+ char openBracket = '\0';
+ char closeBracket = '\0';
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2018-04-09 01:58:07.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2019-07-17 21:44:15.545431576 +0200
+@@ -113,6 +113,8 @@
+ case '⟧': if (direction != null) direction[0] = false; return '⟦';
+ case '⦃': if (direction != null) direction[0] = true; return '⦄';
+ case '⦄': if (direction != null) direction[0] = false; return '⦃';
++ case '⟪': if (direction != null) direction[0] = true; return '⟫';
++ case '⟫': if (direction != null) direction[0] = false; return '⟪';
+ default: return '\0';
+ }
+ } //}}}