merged

--- 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

--- 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

--- 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.

--- 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

--- 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

--- 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

--- 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>\<open>Utilities~/ Global
   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, 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!
 \<close>
@@ -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>\<open>shortcut\<close>
-  properties in \<^file>\<open>$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props\<close>).
+  (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
+  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
 \<close>
 
 
@@ -671,10 +670,11 @@
   wrapper, in contrast to @{tool jedit} run from the command line
   (\secref{sec:command-line}).
 
-  Isabelle/jEdit imitates \<^verbatim>\<open>$ISABELLE_HOME\<close> and \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> 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>\<open>Favorites\<close> 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>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,
+  \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for
+  these two important locations.
 
   \<^medskip>
   Path specifications in prover input or output usually include formal markup

--- 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")
       }
     }

--- 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
+  }
 }

--- 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"

--- 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);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.keymap-merge">
+	  <CODE>
+	    isabelle.jedit.Keymap_Merge.check_dialog(view);
+	  </CODE>
+	</ACTION>
 </ACTIONS>

--- 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

--- /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>" + HTML.output(shortcut.toString) + "</html>"
+      else
+        "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
+          HTML.output("--- " + shortcut.toString) +
+        "</font></html>"
+  }
+
+  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()
+  }
+}

--- 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