# HG changeset patch
# User wenzelm
# Date 1472738722 -7200
# Node ID 9c8a366778e1667a293f6dc09fcc9415ff7f1105
# Parent  4fe8cfaeb1fcd83f3be3f9fe5ab16c02cc434f2a
more robust persistent storage;
tuned;

diff -r 4fe8cfaeb1fc -r 9c8a366778e1 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 15:29:08 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 16:05:22 2016 +0200
@@ -53,12 +53,9 @@
     def is_ignored(keymap_name: String): Boolean =
       ignored_keymaps().contains(keymap_name)
 
-    def ignore(keymap_name: String, b: Boolean)
+    def ignore(keymap_name: String)
     {
-      val keymaps1 =
-        if (b) Library.insert(keymap_name)(ignored_keymaps()).sorted
-        else Library.remove(keymap_name)(ignored_keymaps())
-
+      val keymaps1 = Library.insert(keymap_name)(ignored_keymaps()).sorted
       if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
       else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
     }
@@ -143,7 +140,8 @@
           entry.tail.foreach(i => entries(i).shortcut.reset(keymap))
           entry.shortcut.set(keymap)
         }
-        entry.shortcut.ignore(keymap_name, !b)
+        else
+          entry.shortcut.ignore(keymap_name)
       }
     }
 
@@ -229,8 +227,6 @@
         case keymap => keymap
       }
 
-    var save = false
-
     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)
@@ -255,19 +251,12 @@
           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)
-      save = true
-    }
+    { table_model.apply(keymap_name, keymap) }
+
+    no_shortcut_conflicts.foreach(_.set(keymap))
 
-    if (no_shortcut_conflicts.nonEmpty) {
-      no_shortcut_conflicts.foreach(_.set(keymap))
-      save = true
-    }
-
-    if (save) {
-      keymap_manager.reload()
-      jEdit.saveSettings()
-    }
+    keymap.save()
+    keymap_manager.reload()
+    jEdit.saveSettings()
   }
 }