# HG changeset patch
# User wenzelm
# Date 1472735894 -7200
# Node ID ebcc70c120a9f3609f6f77c29fa9a5043612bfb9
# Parent  b9b5a0ab54eefdc3d49c13c80e280d5cba10267a
separate action;
tuned message;

diff -r b9b5a0ab54ee -r ebcc70c120a9 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Thu Sep 01 14:57:36 2016 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Thu Sep 01 15:18:14 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>
diff -r b9b5a0ab54ee -r ebcc70c120a9 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 14:57:36 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 15:18:14 2016 +0200
@@ -16,7 +16,7 @@
 
 import scala.collection.JavaConversions
 
-import org.gjt.sp.jedit.{jEdit, GUIUtilities}
+import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
 import org.jedit.keymap.{KeymapManager, Keymap}
 
 
@@ -217,7 +217,7 @@
 
   /** check with optional dialog **/
 
-  def check_dialog()
+  def check_dialog(view: View)
   {
     GUI_Thread.require {}
 
@@ -247,13 +247,14 @@
     val table_model = new Table_Model(table_entries)
 
     if (table_entries.nonEmpty &&
-        GUI.confirm_dialog(jEdit.getActiveView,
+        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.") == 0)
+          "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)
       save = true
diff -r b9b5a0ab54ee -r ebcc70c120a9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 14:57:36 2016 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 15:18:14 2016 +0200
@@ -333,7 +333,7 @@
               "It is for testing only, not for production use.")
           }
 
-          Keymap_Merge.check_dialog()
+          Keymap_Merge.check_dialog(jEdit.getActiveView())
 
           Session_Build.session_build(jEdit.getActiveView())