# HG changeset patch # User wenzelm # Date 1563395060 -7200 # Node ID af25255bda02ddbf524dffb0cd2bf41e0042964e # Parent 81b65ddac59fae8ceaa40402745e6daa7f307ea0# Parent 2e8af171887fe43152e1fb72fe2677c8922da827 merged; diff -r 81b65ddac59f -r af25255bda02 Admin/components/components.sha1 --- 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 diff -r 81b65ddac59f -r af25255bda02 Admin/components/main --- 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 diff -r 81b65ddac59f -r af25255bda02 Admin/isabelle_fonts/IsabelleSymbols.sfd --- 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 diff -r 81b65ddac59f -r af25255bda02 Admin/isabelle_fonts/IsabelleSymbolsBold.sfd --- 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 diff -r 81b65ddac59f -r af25255bda02 Admin/isabelle_fonts/README --- 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 ---------------------------------------------------------------------------- diff -r 81b65ddac59f -r af25255bda02 etc/symbols --- 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 @@ \ code: 0x0021d5 group: arrow \ code: 0x0027e8 group: punctuation abbrev: << \ code: 0x0027e9 group: punctuation abbrev: >> +\ code: 0x0027ea group: punctuation abbrev: << +\ code: 0x0027eb group: punctuation abbrev: >> \ code: 0x002308 group: punctuation abbrev: [. \ code: 0x002309 group: punctuation abbrev: .] \ code: 0x00230a group: punctuation abbrev: [. @@ -278,6 +280,7 @@ \ code: 0x00227d group: relation \ code: 0x002225 group: punctuation abbrev: || \ code: 0x0000a6 group: punctuation abbrev: || +\ code: 0x002aff group: punctuation abbrev: || \ code: 0x0000b1 group: operator \ code: 0x002213 group: operator \ code: 0x0000d7 group: operator abbrev: <*> @@ -328,6 +331,7 @@ \ code: 0x0000ae \ code: 0x002010 group: punctuation \ code: 0x0000af group: operator +\ code: 0x0000b7 group: punctuation \ code: 0x0000bc group: digit \ code: 0x0000bd group: digit \ code: 0x0000be group: digit diff -r 81b65ddac59f -r af25255bda02 lib/texinputs/isabelle.sty --- 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}{% diff -r 81b65ddac59f -r af25255bda02 lib/texinputs/isabellesym.sty --- 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}} diff -r 81b65ddac59f -r af25255bda02 src/Pure/Admin/build_fonts.scala --- 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 diff -r 81b65ddac59f -r af25255bda02 src/Tools/jEdit/patches/brackets --- /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'; + } + } //}}}