src/Tools/jEdit/src/keymap_merge.scala

       Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
 
     def is_ignored(keymap_name: String): Boolean =
       ignored_keymaps().contains(keymap_name)
 
-    def ignore(keymap_name: String, b: Boolean)
-    {
-      val keymaps1 =
-        if (b) Library.insert(keymap_name)(ignored_keymaps()).sorted
-        else Library.remove(keymap_name)(ignored_keymaps())
-
+    def ignore(keymap_name: String)
+    {
+      val keymaps1 = Library.insert(keymap_name)(ignored_keymaps()).sorted
       if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
       else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
     }
 
     def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding)

         val b = is_selected(row)
         if (b) {
           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)
       }
     }
 
     override def getColumnCount: Int = 2
 

       keymap_manager.getKeymap(keymap_name) match {
         case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
         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)
 
     val table_entries =

           "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)
-    {
-      table_model.apply(keymap_name, keymap)
-      save = true
-    }
-
-    if (no_shortcut_conflicts.nonEmpty) {
-      no_shortcut_conflicts.foreach(_.set(keymap))
-      save = true
-    }
-
-    if (save) {
-      keymap_manager.reload()
-      jEdit.saveSettings()
-    }
+    { table_model.apply(keymap_name, keymap) }
+
+    no_shortcut_conflicts.foreach(_.set(keymap))
+
+    keymap.save()
+    keymap_manager.reload()
+    jEdit.saveSettings()
   }
 }