--- a/src/Tools/jEdit/src/keymap_merge.scala Thu Sep 01 16:13:46 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala Thu Sep 01 17:35:01 2016 +0200
@@ -246,11 +246,11 @@
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) + ".",
+ "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)
+ "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)
{ table_model.apply(keymap_name, keymap) }
no_shortcut_conflicts.foreach(_.set(keymap))