# HG changeset patch
# User wenzelm
# Date 1472730173 -7200
# Node ID a406d7ab54ce22d72f66ca81b85e9d1de7112292
# Parent  beebcfc745d3825289c37f6c5561bf8d98cf7e00
actual actions;
tuned;

diff -r beebcfc745d3 -r a406d7ab54ce src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 11:55:02 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 13:42:53 2016 +0200
@@ -86,23 +86,16 @@
 
   def get_keymap(): (String, Keymap) =
   {
-    val manager = jEdit.getKeymapManager
+    val keymap_manager = jEdit.getKeymapManager
     val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
     val keymap =
-      manager.getKeymap(keymap_name) match {
-        case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
+      keymap_manager.getKeymap(keymap_name) match {
+        case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
         case keymap => keymap
       }
     (keymap_name, keymap)
   }
 
-  def change_keymap(keymap: Keymap, entry: (Shortcut, List[Shortcut]))
-  {
-    val (shortcut, conflicts) = entry
-    conflicts.foreach(s => keymap.setShortcut(s.property, ""))
-    keymap.setShortcut(shortcut.property, shortcut.binding)
-  }
-
   def get_shortcut_conflicts(keymap: Keymap): List[(Shortcut, List[Shortcut])] =
   {
     val keymap_shortcuts =
@@ -146,11 +139,30 @@
       Synchronized[Set[Int]](
         (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
 
-    private def select(head: Int, tail: List[Int], b: Boolean)
+    def is_selected(row: Int): Boolean = selected.value.contains(row)
+
+    def select(head: Int, tail: List[Int], b: Boolean)
     {
       selected.change(set => if (b) set + head -- tail else set - head ++ tail)
     }
 
+    def apply(keymap_name: String, keymap: Keymap)
+    {
+      GUI_Thread.require {}
+
+      for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
+        val b = is_selected(row)
+        if (b) {
+          entry.tail.foreach(i => keymap.setShortcut(entries(i).shortcut.property, null))
+          keymap.setShortcut(entry.shortcut.property, entry.shortcut.binding)
+        }
+        entry.shortcut.update_ignored(keymap_name, !b)
+      }
+
+      jEdit.getKeymapManager.reload()
+      jEdit.saveSettings()
+    }
+
     override def getColumnCount: Int = 2
 
     override def getColumnClass(i: Int): Class[_ <: Object] =
@@ -164,7 +176,7 @@
     override def getValueAt(row: Int, column: Int): AnyRef =
     {
       get_entry(row) match {
-        case Some(entry) if column == 0 => JBoolean.valueOf(selected.value.contains(row))
+        case Some(entry) if column == 0 => JBoolean.valueOf(is_selected(row))
         case Some(entry) if column == 1 => entry
         case _ => null
       }
@@ -204,12 +216,15 @@
 
     val pending_conflicts =
       shortcut_conflicts.filter({ case (s, cs) => !s.is_ignored(keymap_name) && cs.nonEmpty })
-    if (pending_conflicts.nonEmpty) new Dialog(view, pending_conflicts)
+    if (pending_conflicts.nonEmpty) new Dialog(view, keymap_name, keymap, pending_conflicts)
     // FIXME else silent change
   }
 
-  private class Dialog(view: View, shortcut_conflicts: List[(Shortcut, List[Shortcut])])
-    extends JDialog(view)
+  private class Dialog(
+    view: View,
+    keymap_name: String,
+    keymap: Keymap,
+    shortcut_conflicts: List[(Shortcut, List[Shortcut])]) extends JDialog(view)
   {
     /* table */
 
@@ -253,11 +268,11 @@
     /* buttons */
 
     val ok_button = new Button("OK") {
-      reactions += { case ButtonClicked(_) => close() }  // FIXME
+      reactions += { case ButtonClicked(_) => table_model.apply(keymap_name, keymap); close() }
     }
 
     val cancel_button = new Button("Cancel") {
-      reactions += { case ButtonClicked(_) => close() }  // FIXME
+      reactions += { case ButtonClicked(_) => close() }
     }
 
     private def close()