# HG changeset patch # User wenzelm # Date 1472739226 -7200 # Node ID 79f11158dcc41990fa0e85790f1e048d3289ca4f # Parent 622b54bbe8d4d9c98265cd2450630356f1854f6e# Parent 300f9782cb6fe3c88063ef75d1aa5d3a5bc24b47 merged diff -r 622b54bbe8d4 -r 79f11158dcc4 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Sep 01 14:38:44 2016 +0200 +++ b/Admin/components/components.sha1 Thu Sep 01 16:13:46 2016 +0200 @@ -48,6 +48,7 @@ 878536aab1eaf1a52da560c20bb41ab942971fa3 isabelle_fonts-20160227.tar.gz 8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz 9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz +620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz 8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz 38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz diff -r 622b54bbe8d4 -r 79f11158dcc4 Admin/components/main --- a/Admin/components/main Thu Sep 01 14:38:44 2016 +0200 +++ b/Admin/components/main Thu Sep 01 16:13:46 2016 +0200 @@ -4,7 +4,7 @@ cvc4-1.5pre-3 e-1.8 Haskabelle-2015 -isabelle_fonts-20160812-1 +isabelle_fonts-20160830 jdk-8u102 jedit_build-20160330 jfreechart-1.0.14-1 diff -r 622b54bbe8d4 -r 79f11158dcc4 NEWS --- a/NEWS Thu Sep 01 14:38:44 2016 +0200 +++ b/NEWS Thu Sep 01 16:13:46 2016 +0200 @@ -120,6 +120,13 @@ occurences of the formal entity at the caret position. This facilitates systematic renaming. +* Action "isabelle.keymap-merge" asks the user to resolve pending +Isabelle keymap changes that are in conflict with the current jEdit +keymap; non-conflicting changes are always applied implicitly. This +action is automatically invoked on Isabelle/jEdit startup and thus +increases chances that users see new keyboard shortcuts when re-using +old keymaps. + * Document markup works across multiple Isar commands, e.g. the results established at the end of a proof are properly identified in the theorem statement. diff -r 622b54bbe8d4 -r 79f11158dcc4 etc/symbols --- a/etc/symbols Thu Sep 01 14:38:44 2016 +0200 +++ b/etc/symbols Thu Sep 01 16:13:46 2016 +0200 @@ -385,3 +385,4 @@ \<^dir> code: 0x01F5C0 group: icon font: IsabelleText \<^url> code: 0x01F310 group: icon font: IsabelleText \<^doc> code: 0x01F4D3 group: icon font: IsabelleText +\<^action> code: 0x00261b group: icon font: IsabelleText diff -r 622b54bbe8d4 -r 79f11158dcc4 lib/fonts/IsabelleText.sfd --- a/lib/fonts/IsabelleText.sfd Thu Sep 01 14:38:44 2016 +0200 +++ b/lib/fonts/IsabelleText.sfd Thu Sep 01 16:13:46 2016 +0200 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050361371 -ModificationTime: 1471012141 +ModificationTime: 1472550975 PfmFamily: 17 TTFWeight: 400 TTFWidth: 5 @@ -2241,11 +2241,11 @@ DisplaySize: -96 AntiAlias: 1 FitToEm: 1 -WinInfo: 128340 18 16 +WinInfo: 9684 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 1408 +BeginChars: 1114189 1409 StartChar: u10000 Encoding: 65536 65536 0 @@ -62747,5 +62747,53 @@ 841 238.4 l 1,54,-1 EndSplineSet EndChar + +StartChar: uni261B +Encoding: 9755 9755 1408 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +105 270 m 1,0,-1 + 48 1046 l 1,1,2 + 48 1088 48 1088 71.5 1117 c 128,-1,3 + 95 1146 95 1146 127 1146 c 2,4,-1 + 412 1146 l 2,5,6 + 445 1146 445 1146 468 1117 c 0,7,8 + 481 1101 481 1101 487 1080 c 1,9,-1 + 1105 1080 l 2,10,11 + 1125 1080 1125 1080 1144 1068 c 128,-1,12 + 1163 1056 1163 1056 1174 1032 c 128,-1,13 + 1185 1008 1185 1008 1185 982 c 0,14,15 + 1185 941 1185 941 1161.5 912.5 c 128,-1,16 + 1138 884 1138 884 1105 884 c 2,17,-1 + 522 884 l 1,18,-1 + 524 875 l 1,19,-1 + 781 875 l 1,20,21 + 798 873 798 873 813 862 c 0,22,23 + 832 849 832 849 843.5 825.5 c 128,-1,24 + 855 802 855 802 855 778 c 0,25,26 + 855 737 855 737 831 708.5 c 128,-1,27 + 807 680 807 680 756 680 c 2,28,-1 + 560 680 l 1,29,-1 + 561 670 l 1,30,-1 + 698 670 l 2,31,32 + 717 670 717 670 736.5 657 c 128,-1,33 + 756 644 756 644 767 620.5 c 128,-1,34 + 778 597 778 597 778 572 c 0,35,36 + 778 531 778 531 754 502 c 0,37,38 + 735 478 735 478 699 476 c 1,39,-1 + 596 476 l 1,40,-1 + 599 465 l 1,41,-1 + 640 465 l 1,42,43 + 654 462 654 462 668 453 c 0,44,45 + 687 441 687 441 697.5 417.5 c 128,-1,46 + 708 394 708 394 708 368 c 0,47,48 + 708 328 708 328 685 299 c 128,-1,49 + 662 270 662 270 629 270 c 2,50,-1 + 105 270 l 1,0,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 622b54bbe8d4 -r 79f11158dcc4 lib/fonts/IsabelleTextBold.sfd --- a/lib/fonts/IsabelleTextBold.sfd Thu Sep 01 14:38:44 2016 +0200 +++ b/lib/fonts/IsabelleTextBold.sfd Thu Sep 01 16:13:46 2016 +0200 @@ -20,7 +20,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050374980 -ModificationTime: 1471012188 +ModificationTime: 1472550922 PfmFamily: 17 TTFWeight: 700 TTFWidth: 5 @@ -1678,10 +1678,10 @@ DisplaySize: -96 AntiAlias: 1 FitToEm: 1 -WinInfo: 127638 21 15 +WinInfo: 9513 21 15 BeginPrivate: 0 EndPrivate -BeginChars: 1114115 1400 +BeginChars: 1114115 1401 StartChar: .notdef Encoding: 1114112 -1 0 @@ -68861,87 +68861,87 @@ LayerCount: 2 Fore SplineSet -1611.8 762 m 0 - 1611.8 444.06 1611.8 444.06 1386.86 219.138 c 0 - 1161.91 -5.7998 1161.91 -5.7998 844 -5.7998 c 0 - 526.07 -5.7998 526.07 -5.7998 301.138 219.138 c 0 - 76.2 444.08 76.2 444.08 76.2 762 c 0 - 76.2 1079.91 76.2 1079.91 301.138 1304.86 c 0 - 526.056 1529.8 526.056 1529.8 844 1529.8 c 0 - 1161.93 1529.8 1161.93 1529.8 1386.86 1304.86 c 0 - 1611.8 1079.93 1611.8 1079.93 1611.8 762 c 0 -1220.07 1261.11 m 1 - 1168.47 1300.23 1168.47 1300.23 1111.45 1327.2 c 1 - 1138.31 1275.55 1138.31 1275.55 1161.39 1221.76 c 1 - 1191.78 1240.21 1191.78 1240.21 1220.07 1261.11 c 1 -1465.7 833.3 m 1 - 1446.04 1018.25 1446.04 1018.25 1325.54 1161.18 c 1 - 1272.9 1119.91 1272.9 1119.91 1212.62 1085.87 c 1 - 1254.19 954.411 1254.19 954.411 1263.99 833.3 c 1 - 1465.7 833.3 l 1 -1032.07 1159.49 m 1 - 982.764 1277 982.764 1277 915.3 1379.54 c 1 - 915.3 1128.35 l 1 - 972.667 1137.3 972.667 1137.3 1032.07 1159.49 c 1 -772 1128.4 m 1 - 772 1378.3 l 1 - 705.395 1276.11 705.395 1276.11 656.076 1159.43 c 1 - 715.641 1137.24 715.641 1137.24 772 1128.4 c 1 -1120.11 833.3 m 1 - 1111.28 924.649 1111.28 924.649 1081.23 1024.49 c 1 - 996.9 993.412 996.9 993.412 915.3 983.737 c 1 - 915.3 833.3 l 1 - 1120.11 833.3 l 1 -1465.7 690 m 1 - 1263.98 690 l 1 - 1254.16 569.491 1254.16 569.491 1212.56 437.946 c 1 - 1272.5 403.924 1272.5 403.924 1325.48 362.623 c 1 - 1446.03 505.147 1446.03 505.147 1465.7 690 c 1 -576.794 1327.31 m 1 - 519.517 1300.22 519.517 1300.22 467.933 1261.11 c 1 - 496.214 1240.21 496.214 1240.21 526.679 1221.72 c 1 - 549.892 1275.64 549.892 1275.64 576.794 1327.31 c 1 -772 833.3 m 1 - 772 983.765 l 1 - 690.418 993.615 690.418 993.615 606.766 1024.48 c 1 - 576.71 924.621 576.71 924.621 567.891 833.3 c 1 - 772 833.3 l 1 -1120.09 690 m 1 - 915.3 690 l 1 - 915.3 540.263 l 1 - 996.899 530.588 996.899 530.588 1081.24 499.506 c 1 - 1111.27 599.254 1111.27 599.254 1120.09 690 c 1 -1220.07 262.892 m 1 - 1191.78 283.795 1191.78 283.795 1161.32 302.281 c 1 - 1138.12 248.387 1138.12 248.387 1111.21 196.689 c 1 - 1168.47 223.77 1168.47 223.77 1220.07 262.892 c 1 -475.438 1086.05 m 1 - 415.516 1120.07 415.516 1120.07 362.518 1161.37 c 1 - 241.972 1018.79 241.972 1018.79 222.285 833.3 c 1 - 424.006 833.3 l 1 - 433.81 954.411 433.81 954.411 475.438 1086.05 c 1 -772 540.235 m 1 - 772 690 l 1 - 567.914 690 l 1 - 576.734 599.257 576.734 599.257 606.761 499.515 c 1 - 690.429 530.386 690.429 530.386 772 540.235 c 1 -1031.92 364.563 m 1 - 972.259 386.759 972.259 386.759 915.3 395.651 c 1 - 915.3 144.624 l 1 - 982.429 247.46 982.429 247.46 1031.92 364.563 c 1 -772 145.521 m 1 - 772 395.601 l 1 - 715.225 386.699 715.225 386.699 655.924 364.514 c 1 - 704.843 247.924 704.843 247.924 772 145.521 c 1 -475.435 437.946 m 1 - 433.833 569.489 433.833 569.489 424.022 690 c 1 - 222.315 690 l 1 - 241.994 505.692 241.994 505.692 362.578 362.672 c 1 - 415.516 403.933 415.516 403.933 475.435 437.946 c 1 -576.794 196.689 m 1 - 549.878 248.388 549.878 248.388 526.679 302.281 c 1 - 496.212 283.788 496.212 283.788 467.933 262.892 c 1 - 519.514 223.78 519.514 223.78 576.794 196.689 c 1 +1611.8 762 m 0,0,1 + 1611.8 444.06 1611.8 444.06 1386.86 219.138 c 0,2,3 + 1161.91 -5.7998 1161.91 -5.7998 844 -5.7998 c 0,4,5 + 526.07 -5.7998 526.07 -5.7998 301.138 219.138 c 0,6,7 + 76.2 444.08 76.2 444.08 76.2 762 c 0,8,9 + 76.2 1079.91 76.2 1079.91 301.138 1304.86 c 0,10,11 + 526.056 1529.8 526.056 1529.8 844 1529.8 c 0,12,13 + 1161.93 1529.8 1161.93 1529.8 1386.86 1304.86 c 0,14,15 + 1611.8 1079.93 1611.8 1079.93 1611.8 762 c 0,0,1 +1220.07 1261.11 m 1,16,17 + 1168.47 1300.23 1168.47 1300.23 1111.45 1327.2 c 1,18,19 + 1138.31 1275.55 1138.31 1275.55 1161.39 1221.76 c 1,20,21 + 1191.78 1240.21 1191.78 1240.21 1220.07 1261.11 c 1,16,17 +1465.7 833.3 m 1,22,23 + 1446.04 1018.25 1446.04 1018.25 1325.54 1161.18 c 1,24,25 + 1272.9 1119.91 1272.9 1119.91 1212.62 1085.87 c 1,26,27 + 1254.19 954.411 1254.19 954.411 1263.99 833.3 c 1,28,-1 + 1465.7 833.3 l 1,22,23 +1032.07 1159.49 m 1,29,30 + 982.764 1277 982.764 1277 915.3 1379.54 c 1,31,-1 + 915.3 1128.35 l 1,32,33 + 972.667 1137.3 972.667 1137.3 1032.07 1159.49 c 1,29,30 +772 1128.4 m 1,34,-1 + 772 1378.3 l 1,35,36 + 705.395 1276.11 705.395 1276.11 656.076 1159.43 c 1,37,38 + 715.641 1137.24 715.641 1137.24 772 1128.4 c 1,34,-1 +1120.11 833.3 m 1,39,40 + 1111.28 924.649 1111.28 924.649 1081.23 1024.49 c 1,41,42 + 996.9 993.412 996.9 993.412 915.3 983.737 c 1,43,-1 + 915.3 833.3 l 1,44,-1 + 1120.11 833.3 l 1,39,40 +1465.7 690 m 1,45,-1 + 1263.98 690 l 1,46,47 + 1254.16 569.491 1254.16 569.491 1212.56 437.946 c 1,48,49 + 1272.5 403.924 1272.5 403.924 1325.48 362.623 c 1,50,51 + 1446.03 505.147 1446.03 505.147 1465.7 690 c 1,45,-1 +576.794 1327.31 m 1,52,53 + 519.517 1300.22 519.517 1300.22 467.933 1261.11 c 1,54,55 + 496.214 1240.21 496.214 1240.21 526.679 1221.72 c 1,56,57 + 549.892 1275.64 549.892 1275.64 576.794 1327.31 c 1,52,53 +772 833.3 m 1,58,-1 + 772 983.765 l 1,59,60 + 690.418 993.615 690.418 993.615 606.766 1024.48 c 1,61,62 + 576.71 924.621 576.71 924.621 567.891 833.3 c 1,63,-1 + 772 833.3 l 1,58,-1 +1120.09 690 m 1,64,-1 + 915.3 690 l 1,65,-1 + 915.3 540.263 l 1,66,67 + 996.899 530.588 996.899 530.588 1081.24 499.506 c 1,68,69 + 1111.27 599.254 1111.27 599.254 1120.09 690 c 1,64,-1 +1220.07 262.892 m 1,70,71 + 1191.78 283.795 1191.78 283.795 1161.32 302.281 c 1,72,73 + 1138.12 248.387 1138.12 248.387 1111.21 196.689 c 1,74,75 + 1168.47 223.77 1168.47 223.77 1220.07 262.892 c 1,70,71 +475.438 1086.05 m 1,76,77 + 415.516 1120.07 415.516 1120.07 362.518 1161.37 c 1,78,79 + 241.972 1018.79 241.972 1018.79 222.285 833.3 c 1,80,-1 + 424.006 833.3 l 1,81,82 + 433.81 954.411 433.81 954.411 475.438 1086.05 c 1,76,77 +772 540.235 m 1,83,-1 + 772 690 l 1,84,-1 + 567.914 690 l 1,85,86 + 576.734 599.257 576.734 599.257 606.761 499.515 c 1,87,88 + 690.429 530.386 690.429 530.386 772 540.235 c 1,83,-1 +1031.92 364.563 m 1,89,90 + 972.259 386.759 972.259 386.759 915.3 395.651 c 1,91,-1 + 915.3 144.624 l 1,92,93 + 982.429 247.46 982.429 247.46 1031.92 364.563 c 1,89,90 +772 145.521 m 1,94,-1 + 772 395.601 l 1,95,96 + 715.225 386.699 715.225 386.699 655.924 364.514 c 1,97,98 + 704.843 247.924 704.843 247.924 772 145.521 c 1,94,-1 +475.435 437.946 m 1,99,100 + 433.833 569.489 433.833 569.489 424.022 690 c 1,101,-1 + 222.315 690 l 1,102,103 + 241.994 505.692 241.994 505.692 362.578 362.672 c 1,104,105 + 415.516 403.933 415.516 403.933 475.435 437.946 c 1,99,100 +576.794 196.689 m 1,106,107 + 549.878 248.388 549.878 248.388 526.679 302.281 c 1,108,109 + 496.212 283.788 496.212 283.788 467.933 262.892 c 1,110,111 + 519.514 223.78 519.514 223.78 576.794 196.689 c 1,106,107 EndSplineSet EndChar @@ -68953,61 +68953,61 @@ LayerCount: 2 Fore SplineSet -987.6 131.45 m 2 - 987.6 117.46 987.6 117.46 982.253 104.974 c 0 - 976.906 92.4875 976.906 92.4875 973.075 87.9227 c 0 - 969.244 83.3579 969.244 83.3579 960.649 74.2987 c 0 - 951.974 65.1552 951.974 65.1552 947.42 60.9378 c 0 - 942.865 56.7205 942.865 56.7205 929.937 50.7352 c 0 - 917.009 44.75 917.009 44.75 902.3 44.75 c 2 - 154.7 44.75 l 2 - 144.755 44.75 144.755 44.75 136.732 46.5759 c 0 - 128.708 48.4017 128.708 48.4017 123.042 52.0322 c 0 - 117.376 55.6626 117.376 55.6626 114.185 58.3353 c 0 - 110.995 61.0081 110.995 61.0081 107.166 65.5483 c 0 - 103.337 70.0886 103.337 70.0886 102.538 70.8876 c 0 - 101.738 71.6866 101.738 71.6866 97.1983 75.5157 c 0 - 92.6582 79.3449 92.6582 79.3449 89.9854 82.5355 c 0 - 87.3125 85.726 87.3125 85.726 83.6821 91.3921 c 0 - 80.0518 97.0581 80.0518 97.0581 78.2259 105.082 c 0 - 76.4 113.105 76.4 113.105 76.4 123.05 c 2 - 76.4 1202.45 l 2 - 76.4 1246.98 76.4 1246.98 114.258 1277.83 c 0 - 124.181 1285.77 124.181 1285.77 140.128 1292.56 c 0 - 156.075 1299.35 156.075 1299.35 185.287 1307.52 c 0 - 214.5 1315.68 214.5 1315.68 243.971 1322.98 c 0 - 273.442 1330.28 273.442 1330.28 329.44 1344.31 c 0 - 385.437 1358.34 385.437 1358.34 435.927 1371.78 c 0 - 469.093 1380.61 469.093 1380.61 514.719 1392.86 c 0 - 560.345 1405.11 560.345 1405.11 583.654 1411.34 c 0 - 606.963 1417.58 606.963 1417.58 637.85 1425.69 c 0 - 668.737 1433.8 668.737 1433.8 684.766 1437.64 c 0 - 700.795 1441.48 700.795 1441.48 718.697 1445.43 c 0 - 736.599 1449.39 736.599 1449.39 747.103 1450.82 c 0 - 757.606 1452.25 757.606 1452.25 765.1 1452.25 c 0 - 777.132 1452.25 777.132 1452.25 787.664 1450.49 c 0 - 816.159 1445.72 816.159 1445.72 837.129 1423.36 c 0 - 858.1 1400.99 858.1 1400.99 858.1 1370.45 c 2 - 858.1 1285.65 l 1 - 919.1 1285.65 l 2 - 952.854 1285.65 952.854 1285.65 973.808 1252.37 c 0 - 987.6 1230.47 987.6 1230.47 987.6 1210.15 c 2 - 987.6 131.45 l 2 -821.9 210.45 m 1 - 821.9 1122.05 l 1 - 284.8 1122.05 l 1 - 284.8 210.45 l 1 - 821.9 210.45 l 1 -811.2 725.15 m 1 - 302.5 725.15 l 1 - 302.5 1108.55 l 1 - 811.2 1108.55 l 1 - 811.2 725.15 l 1 -678.4 855.15 m 1 - 678.4 978.55 l 1 - 435.3 978.55 l 1 - 435.3 855.15 l 1 - 678.4 855.15 l 1 +987.6 131.45 m 2,0,1 + 987.6 117.46 987.6 117.46 982.253 104.974 c 0,2,3 + 976.906 92.4875 976.906 92.4875 973.075 87.9227 c 0,4,5 + 969.244 83.3579 969.244 83.3579 960.649 74.2987 c 0,6,7 + 951.974 65.1552 951.974 65.1552 947.42 60.9378 c 0,8,9 + 942.865 56.7205 942.865 56.7205 929.937 50.7352 c 0,10,11 + 917.009 44.75 917.009 44.75 902.3 44.75 c 2,12,-1 + 154.7 44.75 l 2,13,14 + 144.755 44.75 144.755 44.75 136.732 46.5759 c 0,15,16 + 128.708 48.4017 128.708 48.4017 123.042 52.0322 c 0,17,18 + 117.376 55.6626 117.376 55.6626 114.185 58.3353 c 0,19,20 + 110.995 61.0081 110.995 61.0081 107.166 65.5483 c 0,21,22 + 103.337 70.0886 103.337 70.0886 102.538 70.8876 c 0,23,24 + 101.738 71.6866 101.738 71.6866 97.1983 75.5157 c 0,25,26 + 92.6582 79.3449 92.6582 79.3449 89.9854 82.5355 c 0,27,28 + 87.3125 85.726 87.3125 85.726 83.6821 91.3921 c 0,29,30 + 80.0518 97.0581 80.0518 97.0581 78.2259 105.082 c 0,31,32 + 76.4 113.105 76.4 113.105 76.4 123.05 c 2,33,-1 + 76.4 1202.45 l 2,34,35 + 76.4 1246.98 76.4 1246.98 114.258 1277.83 c 0,36,37 + 124.181 1285.77 124.181 1285.77 140.128 1292.56 c 0,38,39 + 156.075 1299.35 156.075 1299.35 185.287 1307.52 c 0,40,41 + 214.5 1315.68 214.5 1315.68 243.971 1322.98 c 0,42,43 + 273.442 1330.28 273.442 1330.28 329.44 1344.31 c 0,44,45 + 385.437 1358.34 385.437 1358.34 435.927 1371.78 c 0,46,47 + 469.093 1380.61 469.093 1380.61 514.719 1392.86 c 0,48,49 + 560.345 1405.11 560.345 1405.11 583.654 1411.34 c 0,50,51 + 606.963 1417.58 606.963 1417.58 637.85 1425.69 c 0,52,53 + 668.737 1433.8 668.737 1433.8 684.766 1437.64 c 0,54,55 + 700.795 1441.48 700.795 1441.48 718.697 1445.43 c 0,56,57 + 736.599 1449.39 736.599 1449.39 747.103 1450.82 c 0,58,59 + 757.606 1452.25 757.606 1452.25 765.1 1452.25 c 0,60,61 + 777.132 1452.25 777.132 1452.25 787.664 1450.49 c 0,62,63 + 816.159 1445.72 816.159 1445.72 837.129 1423.36 c 0,64,65 + 858.1 1400.99 858.1 1400.99 858.1 1370.45 c 2,66,-1 + 858.1 1285.65 l 1,67,-1 + 919.1 1285.65 l 2,68,69 + 952.854 1285.65 952.854 1285.65 973.808 1252.37 c 0,70,71 + 987.6 1230.47 987.6 1230.47 987.6 1210.15 c 2,72,-1 + 987.6 131.45 l 2,0,1 +821.9 210.45 m 1,73,-1 + 821.9 1122.05 l 1,74,-1 + 284.8 1122.05 l 1,75,-1 + 284.8 210.45 l 1,76,-1 + 821.9 210.45 l 1,73,-1 +811.2 725.15 m 1,77,-1 + 302.5 725.15 l 1,78,-1 + 302.5 1108.55 l 1,79,-1 + 811.2 1108.55 l 1,80,-1 + 811.2 725.15 l 1,77,-1 +678.4 855.15 m 1,81,-1 + 678.4 978.55 l 1,82,-1 + 435.3 978.55 l 1,83,-1 + 435.3 855.15 l 1,84,-1 + 678.4 855.15 l 1,81,-1 EndSplineSet EndChar @@ -69019,51 +69019,51 @@ LayerCount: 2 Fore SplineSet -1081.5 163.65 m 2 - 1081.5 122.722 1081.5 122.722 1041.85 96.8642 c 0 - 1031.79 90.5761 1031.79 90.5761 1022.36 87.2552 c 0 - 1012.94 83.9343 1012.94 83.9343 1006.68 83.0855 c 0 - 1000.42 82.2367 1000.42 82.2367 986.754 81.065 c 0 - 973.093 79.8932 973.093 79.8932 962.975 78.4862 c 0 - 906.629 70.65 906.629 70.65 890.5 70.65 c 0 - 874.073 70.65 874.073 70.65 856.304 77.2317 c 0 - 838.536 83.8135 838.536 83.8135 824.647 92.1127 c 0 - 810.758 100.412 810.758 100.412 779.459 120.135 c 0 - 748.161 139.858 748.161 139.858 723.008 154.42 c 0 - 580.768 235.396 580.768 235.396 299.885 396.806 c 0 - 258.685 421.253 258.685 421.253 178.198 468.715 c 1 - 153.461 481.015 153.461 481.015 114.61 506.915 c 2 - 110.906 509.385 l 1 - 107.686 512.459 l 2 - 98.597 521.135 98.597 521.135 92.1108 530.717 c 0 - 76.5 553.779 76.5 553.779 76.5 580.15 c 2 - 76.5 1324.95 l 2 - 76.5 1358.02 76.5 1358.02 101.608 1376.08 c 0 - 126.716 1394.15 126.716 1394.15 152.7 1394.15 c 0 - 160.188 1394.15 160.188 1394.15 165.884 1393.16 c 0 - 171.581 1392.17 171.581 1392.17 173.948 1391.19 c 0 - 176.315 1390.21 176.315 1390.21 179.646 1388.28 c 0 - 182.977 1386.34 182.977 1386.34 184.004 1385.86 c 1 - 184.3 1409.27 l 2 - 184.3 1439.75 184.3 1439.75 206.971 1459.85 c 0 - 229.641 1479.96 229.641 1479.96 256.265 1482.17 c 2 - 272.065 1483.49 l 1 - 691.737 1243.39 l 1 - 727.276 1272.51 727.276 1272.51 756.51 1292.71 c 2 - 782.8 1310.87 l 1 - 1081.5 1141.89 l 1 - 1081.5 163.65 l 2 -923.5 948.388 m 1 - 923.5 1050.52 l 1 - 794.39 1125.14 l 1 - 728.336 1074.48 l 2 - 723.943 1071.54 723.943 1071.54 720.835 1068.73 c 1 - 923.5 948.388 l 1 -815 283.379 m 1 - 815 828.882 l 1 - 235.2 1169.98 l 1 - 235.2 617.33 l 1 - 815 283.379 l 1 +1081.5 163.65 m 2,0,1 + 1081.5 122.722 1081.5 122.722 1041.85 96.8642 c 0,2,3 + 1031.79 90.5761 1031.79 90.5761 1022.36 87.2552 c 0,4,5 + 1012.94 83.9343 1012.94 83.9343 1006.68 83.0855 c 0,6,7 + 1000.42 82.2367 1000.42 82.2367 986.754 81.065 c 0,8,9 + 973.093 79.8932 973.093 79.8932 962.975 78.4862 c 0,10,11 + 906.629 70.65 906.629 70.65 890.5 70.65 c 0,12,13 + 874.073 70.65 874.073 70.65 856.304 77.2317 c 0,14,15 + 838.536 83.8135 838.536 83.8135 824.647 92.1127 c 0,16,17 + 810.758 100.412 810.758 100.412 779.459 120.135 c 0,18,19 + 748.161 139.858 748.161 139.858 723.008 154.42 c 0,20,21 + 580.768 235.396 580.768 235.396 299.885 396.806 c 0,22,23 + 258.685 421.253 258.685 421.253 178.198 468.715 c 1,24,25 + 153.461 481.015 153.461 481.015 114.61 506.915 c 2,26,-1 + 110.906 509.385 l 1,27,-1 + 107.686 512.459 l 2,28,29 + 98.597 521.135 98.597 521.135 92.1108 530.717 c 0,30,31 + 76.5 553.779 76.5 553.779 76.5 580.15 c 2,32,-1 + 76.5 1324.95 l 2,33,34 + 76.5 1358.02 76.5 1358.02 101.608 1376.08 c 0,35,36 + 126.716 1394.15 126.716 1394.15 152.7 1394.15 c 0,37,38 + 160.188 1394.15 160.188 1394.15 165.884 1393.16 c 0,39,40 + 171.581 1392.17 171.581 1392.17 173.948 1391.19 c 0,41,42 + 176.315 1390.21 176.315 1390.21 179.646 1388.28 c 0,43,44 + 182.977 1386.34 182.977 1386.34 184.004 1385.86 c 1,45,-1 + 184.3 1409.27 l 2,46,47 + 184.3 1439.75 184.3 1439.75 206.971 1459.85 c 0,48,49 + 229.641 1479.96 229.641 1479.96 256.265 1482.17 c 2,50,-1 + 272.065 1483.49 l 1,51,-1 + 691.737 1243.39 l 1,52,53 + 727.276 1272.51 727.276 1272.51 756.51 1292.71 c 2,54,-1 + 782.8 1310.87 l 1,55,-1 + 1081.5 1141.89 l 1,56,-1 + 1081.5 163.65 l 2,0,1 +923.5 948.388 m 1,57,-1 + 923.5 1050.52 l 1,58,-1 + 794.39 1125.14 l 1,59,-1 + 728.336 1074.48 l 2,60,61 + 723.943 1071.54 723.943 1071.54 720.835 1068.73 c 1,62,-1 + 923.5 948.388 l 1,57,-1 +815 283.379 m 1,63,-1 + 815 828.882 l 1,64,-1 + 235.2 1169.98 l 1,65,-1 + 235.2 617.33 l 1,66,-1 + 815 283.379 l 1,63,-1 EndSplineSet EndChar @@ -69075,46 +69075,94 @@ LayerCount: 2 Fore SplineSet -1165.12 71.72 m 1 - 150.881 71.72 l 1 - 150.881 1462.28 l 1 - 1165.12 1462.28 l 1 - 1165.12 71.72 l 1 -1021.12 215.72 m 1 - 1021.12 1318.28 l 1 - 294.881 1318.28 l 1 - 294.881 215.72 l 1 - 1021.12 215.72 l 1 -999.641 1165.4 m 1 - 316.359 1165.4 l 1 - 316.359 1309.4 l 1 - 999.641 1309.4 l 1 - 999.641 1165.4 l 1 -999.641 977.24 m 1 - 316.359 977.24 l 1 - 316.359 1121.24 l 1 - 999.641 1121.24 l 1 - 999.641 977.24 l 1 -999.641 789.08 m 1 - 316.359 789.08 l 1 - 316.359 933.08 l 1 - 999.641 933.08 l 1 - 999.641 789.08 l 1 -999.641 600.92 m 1 - 316.359 600.92 l 1 - 316.359 744.92 l 1 - 999.641 744.92 l 1 - 999.641 600.92 l 1 -999.641 412.76 m 1 - 316.359 412.76 l 1 - 316.359 556.76 l 1 - 999.641 556.76 l 1 - 999.641 412.76 l 1 -999.641 224.6 m 1 - 316.359 224.6 l 1 - 316.359 368.6 l 1 - 999.641 368.6 l 1 - 999.641 224.6 l 1 +1165.12 71.72 m 1,0,-1 + 150.881 71.72 l 1,1,-1 + 150.881 1462.28 l 1,2,-1 + 1165.12 1462.28 l 1,3,-1 + 1165.12 71.72 l 1,0,-1 +1021.12 215.72 m 1,4,-1 + 1021.12 1318.28 l 1,5,-1 + 294.881 1318.28 l 1,6,-1 + 294.881 215.72 l 1,7,-1 + 1021.12 215.72 l 1,4,-1 +999.641 1165.4 m 1,8,-1 + 316.359 1165.4 l 1,9,-1 + 316.359 1309.4 l 1,10,-1 + 999.641 1309.4 l 1,11,-1 + 999.641 1165.4 l 1,8,-1 +999.641 977.24 m 1,12,-1 + 316.359 977.24 l 1,13,-1 + 316.359 1121.24 l 1,14,-1 + 999.641 1121.24 l 1,15,-1 + 999.641 977.24 l 1,12,-1 +999.641 789.08 m 1,16,-1 + 316.359 789.08 l 1,17,-1 + 316.359 933.08 l 1,18,-1 + 999.641 933.08 l 1,19,-1 + 999.641 789.08 l 1,16,-1 +999.641 600.92 m 1,20,-1 + 316.359 600.92 l 1,21,-1 + 316.359 744.92 l 1,22,-1 + 999.641 744.92 l 1,23,-1 + 999.641 600.92 l 1,20,-1 +999.641 412.76 m 1,24,-1 + 316.359 412.76 l 1,25,-1 + 316.359 556.76 l 1,26,-1 + 999.641 556.76 l 1,27,-1 + 999.641 412.76 l 1,24,-1 +999.641 224.6 m 1,28,-1 + 316.359 224.6 l 1,29,-1 + 316.359 368.6 l 1,30,-1 + 999.641 368.6 l 1,31,-1 + 999.641 224.6 l 1,28,-1 +EndSplineSet +EndChar + +StartChar: uni261B +Encoding: 9755 9755 1400 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +105 270 m 1,0,-1 + 48 1046 l 1,1,2 + 48 1087 48 1087 71.5 1116.5 c 128,-1,3 + 95 1146 95 1146 127 1146 c 2,4,-1 + 412 1146 l 2,5,6 + 445 1146 445 1146 468 1117 c 0,7,8 + 480 1101 480 1101 487 1080 c 1,9,-1 + 1105 1080 l 2,10,11 + 1125 1080 1125 1080 1144 1068 c 128,-1,12 + 1163 1056 1163 1056 1174 1032 c 128,-1,13 + 1185 1008 1185 1008 1185 982 c 0,14,15 + 1185 941 1185 941 1161.5 912.5 c 128,-1,16 + 1138 884 1138 884 1105 884 c 2,17,-1 + 522 884 l 1,18,-1 + 524 875 l 1,19,-1 + 781 875 l 1,20,21 + 798 872 798 872 813 862 c 0,22,23 + 832 849 832 849 843.5 825.5 c 128,-1,24 + 855 802 855 802 855 778 c 0,25,26 + 855 737 855 737 831 708.5 c 128,-1,27 + 807 680 807 680 756 680 c 2,28,-1 + 560 680 l 1,29,-1 + 561 670 l 1,30,-1 + 698 670 l 2,31,32 + 718 670 718 670 737 657 c 128,-1,33 + 756 644 756 644 767 620.5 c 128,-1,34 + 778 597 778 597 778 572 c 0,35,36 + 778 530 778 530 754 502 c 1,37,38 + 735 478 735 478 699 476 c 1,39,-1 + 596 476 l 1,40,-1 + 599 465 l 1,41,-1 + 640 465 l 1,42,43 + 654 462 654 462 668 453 c 0,44,45 + 687 441 687 441 697.5 417.5 c 128,-1,46 + 708 394 708 394 708 368 c 0,47,48 + 708 328 708 328 685 299 c 128,-1,49 + 662 270 662 270 629 270 c 2,50,-1 + 105 270 l 1,0,-1 EndSplineSet EndChar EndChars diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Doc/JEdit/JEdit.thy Thu Sep 01 16:13:46 2016 +0200 @@ -166,8 +166,7 @@ Regular jEdit options are accessible via the dialogs \<^emph>\Utilities~/ Global Options\ or \<^emph>\Plugins~/ Plugin Options\, with a second chance to flip the two within the central options dialog. Changes are stored in @{path - "$ISABELLE_HOME_USER/jedit/properties"} and @{path - "$ISABELLE_HOME_USER/jedit/keymaps"}. + "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}. Isabelle system options are managed by Isabelle/Scala and changes are stored in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of @@ -193,7 +192,7 @@ \<^medskip> Options are usually loaded on startup and saved on shutdown of Isabelle/jEdit. Editing the machine-generated @{path - "$ISABELLE_HOME_USER/jedit/properties"} or @{path + "$JEDIT_SETTINGS/properties"} or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is running is likely to cause surprise due to lost update! \ @@ -212,8 +211,8 @@ Isabelle/jEdit due to various fine-tuning of global defaults, with additional keyboard shortcuts for Isabelle-specific functionality. Users may change their keymap later, but need to copy some keyboard shortcuts manually - (see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\shortcut\ - properties in \<^file>\$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props\). + (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\shortcut\ properties in + \<^file>\$JEDIT_HOME/src/jEdit.props\). \ @@ -671,10 +670,11 @@ wrapper, in contrast to @{tool jedit} run from the command line (\secref{sec:command-line}). - Isabelle/jEdit imitates \<^verbatim>\$ISABELLE_HOME\ and \<^verbatim>\$ISABELLE_HOME_USER\ within - the Java process environment, in order to allow easy access to these - important places from the editor. The file browser of jEdit also includes - \<^emph>\Favorites\ for these two important locations. + Isabelle/jEdit imitates important system settings within the Java process + environment, in order to allow easy access to these important places from + the editor: \<^verbatim>\$ISABELLE_HOME\, \<^verbatim>\$ISABELLE_HOME_USER\, \<^verbatim>\$JEDIT_HOME\, + \<^verbatim>\$JEDIT_SETTINGS\. The file browser of jEdit also includes \<^emph>\Favorites\ for + these two important locations. \<^medskip> Path specifications in prover input or output usually include formal markup diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Pure/Tools/main.scala Thu Sep 01 16:13:46 2016 +0200 @@ -100,11 +100,15 @@ { val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER") + val jedit_home = Isabelle_System.getenv("JEDIT_HOME") + val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS") (env0: Any) => { val env = env0.asInstanceOf[java.util.Map[String, String]] env.put("ISABELLE_HOME", File.platform_path(isabelle_home)) env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user)) + env.put("JEDIT_HOME", File.platform_path(jedit_home)) + env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings)) env.remove("ISABELLE_ROOT") } } diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Pure/library.scala --- a/src/Pure/library.scala Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Pure/library.scala Thu Sep 01 16:13:46 2016 +0200 @@ -187,4 +187,11 @@ def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) + + def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = + { + val result = new mutable.ListBuffer[A] + for (x <- xs if !result.exists(y => eq(x, y))) result += x + result.toList + } } diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 01 16:13:46 2016 +0200 @@ -42,6 +42,7 @@ "src/jedit_options.scala" "src/jedit_resources.scala" "src/jedit_sessions.scala" + "src/keymap_merge.scala" "src/monitor_dockable.scala" "src/output_dockable.scala" "src/pide_docking_framework.scala" diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Tools/jEdit/src/actions.xml Thu Sep 01 16:13:46 2016 +0200 @@ -152,4 +152,9 @@ isabelle.jedit.Isabelle.plugin_options(view); + + + isabelle.jedit.Keymap_Merge.check_dialog(view); + + diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Thu Sep 01 16:13:46 2016 +0200 @@ -184,7 +184,7 @@ gatchan.highlight.overview=false home.shortcut= insert-newline-indent.shortcut= -insert-newline.shortcut=ENTER +insert-newline.shortcut= isabelle-debugger.dock-position=floating isabelle-documentation.dock-position=right isabelle-output.dock-position=bottom @@ -281,6 +281,10 @@ vfs.favorite.0=$ISABELLE_HOME vfs.favorite.1.type=1 vfs.favorite.1=$ISABELLE_HOME_USER +vfs.favorite.2.type=1 +vfs.favorite.2=$JEDIT_HOME +vfs.favorite.3.type=1 +vfs.favorite.3=$JEDIT_SETTINGS view.antiAlias=standard view.blockCaret=true view.caretBlink=false diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Tools/jEdit/src/keymap_merge.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/keymap_merge.scala Thu Sep 01 16:13:46 2016 +0200 @@ -0,0 +1,262 @@ +/* Title: Tools/jEdit/src/keymap_merge.scala + Author: Makarius + +Merge of Isabelle shortcuts vs. jEdit keymap. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.lang.{Class, Boolean => JBoolean} +import java.awt.{Color, Dimension, BorderLayout} +import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane} +import javax.swing.table.AbstractTableModel + +import scala.collection.JavaConversions + +import org.gjt.sp.jedit.{jEdit, View, GUIUtilities} +import org.jedit.keymap.{KeymapManager, Keymap} + + +object Keymap_Merge +{ + /** shortcuts **/ + + private def is_shortcut(property: String): Boolean = + (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && + !property.startsWith("options.shortcuts.") + + class Shortcut(val property: String, val binding: String) + { + override def toString: String = property + "=" + binding + + def primary: Boolean = property.endsWith(".shortcut") + + val action: String = + Library.try_unsuffix(".shortcut", property) orElse + Library.try_unsuffix(".shortcut2", property) getOrElse + error("Bad shortcut property: " + quote(property)) + + val label: String = + GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) + + + /* ignore wrt. keymap */ + + private def prop_ignore: String = property + ".ignore" + + def ignored_keymaps(): List[String] = + Library.space_explode(',', jEdit.getProperty(prop_ignore, "")) + + def is_ignored(keymap_name: String): Boolean = + ignored_keymaps().contains(keymap_name) + + def ignore(keymap_name: String) + { + val keymaps1 = Library.insert(keymap_name)(ignored_keymaps()).sorted + if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore) + else jEdit.setProperty(prop_ignore, keymaps1.mkString(",")) + } + + def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding) + def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null) + } + + + /* content wrt. keymap */ + + def convert_properties(props: java.util.Properties): List[Shortcut] = + if (props == null) Nil + else { + var result = List.empty[Shortcut] + for (entry <- JavaConversions.mapAsScalaMap(props)) { + entry match { + case (a: String, b: String) if is_shortcut(a) => + result ::= new Shortcut(a, b) + case _ => + } + } + result.sortBy(_.property) + } + + def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] = + { + val keymap_shortcuts = + if (keymap == null) Nil + else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) + + for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield { + val conflicts = + keymap_shortcuts.filter(s1 => + s.property == s1.property && s.binding != s1.binding || + s.property != s1.property && s.binding == s1.binding && s1.binding != "") + (s, conflicts) + } + } + + + + /** table **/ + + private def conflict_color: Color = + PIDE.options.color_value("error_color") + + private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) + { + override def toString: String = + if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" + else + "" + + HTML.output("--- " + shortcut.toString) + + "" + } + + private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel + { + private val entries_count = entries.length + private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count + private def get_entry(row: Int): Option[Table_Entry] = + if (has_entry(row)) Some(entries(row)) else None + + private val selected = + Synchronized[Set[Int]]( + (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet) + + private def is_selected(row: Int): Boolean = + selected.value.contains(row) + + private def select(head: Int, tail: List[Int], b: Boolean): Unit = + selected.change(set => if (b) set + head -- tail else set - head ++ tail) + + def apply(keymap_name: String, keymap: Keymap) + { + GUI_Thread.require {} + + for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { + val b = is_selected(row) + if (b) { + entry.tail.foreach(i => entries(i).shortcut.reset(keymap)) + entry.shortcut.set(keymap) + } + else + entry.shortcut.ignore(keymap_name) + } + } + + override def getColumnCount: Int = 2 + + override def getColumnClass(i: Int): Class[_ <: Object] = + if (i == 0) classOf[JBoolean] else classOf[Object] + + override def getColumnName(i: Int): String = + if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" + + override def getRowCount: Int = entries_count + + override def getValueAt(row: Int, column: Int): AnyRef = + { + get_entry(row) match { + case Some(entry) if column == 0 => JBoolean.valueOf(is_selected(row)) + case Some(entry) if column == 1 => entry + case _ => null + } + } + + override def isCellEditable(row: Int, column: Int): Boolean = + has_entry(row) && column == 0 + + override def setValueAt(value: AnyRef, row: Int, column: Int) + { + value match { + case obj: JBoolean if has_entry(row) && column == 0 => + val b = obj.booleanValue + val entry = entries(row) + entry.head match { + case None => select(row, entry.tail, b) + case Some(head_row) => + val head_entry = entries(head_row) + select(head_row, head_entry.tail, !b) + } + GUI_Thread.later { fireTableDataChanged() } + case _ => + } + } + } + + private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) + { + private val cell_size = GUIUtilities.defaultTableCellSize() + private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) + + val table = new JTable(table_model) + table.setShowGrid(false) + table.setIntercellSpacing(new Dimension(0, 0)) + table.setRowHeight(cell_size.height + 2) + table.setPreferredScrollableViewportSize(table_size) + table.setFillsViewportHeight(true) + table.getTableHeader.setReorderingAllowed(false) + + table.getColumnModel.getColumn(0).setPreferredWidth(30) + table.getColumnModel.getColumn(0).setMinWidth(30) + table.getColumnModel.getColumn(0).setMaxWidth(30) + table.getColumnModel.getColumn(0).setResizable(false) + table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30) + + val scroller = new JScrollPane(table) + scroller.getViewport.setBackground(table.getBackground) + scroller.setPreferredSize(table_size) + + add(scroller, BorderLayout.CENTER) + } + + + + /** check with optional dialog **/ + + def check_dialog(view: View) + { + GUI_Thread.require {} + + val keymap_manager = jEdit.getKeymapManager + val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) + val keymap = + keymap_manager.getKeymap(keymap_name) match { + case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) + case keymap => keymap + } + + val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap) + val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s + val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty) + + val table_entries = + for { + ((shortcut, conflicts), i) <- shortcut_conflicts zip + shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length }) + entry <- + Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: + conflicts.map(Table_Entry(_, Some(i), Nil)) + } yield entry + + val table_model = new Table_Model(table_entries) + + if (table_entries.nonEmpty && + GUI.confirm_dialog(view, + "Pending Isabelle/jEdit keymap changes", + JOptionPane.OK_CANCEL_OPTION, + "The following Isabelle keymap changes are in conflict with", + "the current jEdit keymap " + quote(keymap_name) + ".", + new Table(table_model), + "Selected shortcuts will be applied, unselected changes will be ignored.", + "Results are made persistent in $JEDIT_SETTINGS/properties.") == 0) + { table_model.apply(keymap_name, keymap) } + + no_shortcut_conflicts.foreach(_.set(keymap)) + + keymap.save() + keymap_manager.reload() + jEdit.saveSettings() + } +} diff -r 622b54bbe8d4 -r 79f11158dcc4 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Sep 01 14:38:44 2016 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Thu Sep 01 16:13:46 2016 +0200 @@ -333,6 +333,8 @@ "It is for testing only, not for production use.") } + Keymap_Merge.check_dialog(jEdit.getActiveView()) + Session_Build.session_build(jEdit.getActiveView()) case msg: BufferUpdate