src/Tools/jEdit/src/keymap_merge.scala
changeset 63753 c57db6b2befc
parent 63750 9c8a366778e1
child 63759 f81e5f492cf9
     1.1 --- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 16:13:46 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 17:35:01 2016 +0200
     1.3 @@ -246,11 +246,11 @@
     1.4          GUI.confirm_dialog(view,
     1.5            "Pending Isabelle/jEdit keymap changes",
     1.6            JOptionPane.OK_CANCEL_OPTION,
     1.7 -          "The following Isabelle keymap changes are in conflict with",
     1.8 -          "the current jEdit keymap " + quote(keymap_name) + ".",
     1.9 +          "The following Isabelle keymap changes are in conflict with the current",
    1.10 +          "jEdit keymap " + quote(keymap_name) + ".",
    1.11            new Table(table_model),
    1.12            "Selected shortcuts will be applied, unselected changes will be ignored.",
    1.13 -          "Results are made persistent in $JEDIT_SETTINGS/properties.") == 0)
    1.14 +          "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)
    1.15      { table_model.apply(keymap_name, keymap) }
    1.16  
    1.17      no_shortcut_conflicts.foreach(_.set(keymap))