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