clarified GUI;
authorwenzelm
Wed, 31 Aug 2016 21:25:54 +0200
changeset 63742 7b2963b11e4a
parent 63741 352a257fa13a
child 63743 10c08a4d39dd
clarified GUI;
src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Wed Aug 31 20:35:15 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Wed Aug 31 21:25:54 2016 +0200
@@ -125,10 +125,10 @@
   private def conflict_color: Color =
     PIDE.options.color_value("error_color")
 
-  private sealed case class Table_Entry(shortcut: Shortcut, head: Boolean)
+  private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int])
   {
     override def toString: String =
-      if (head) "<html>" + HTML.output(shortcut.toString) + "</html>"
+      if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
       else
         "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
           HTML.output("--- " + shortcut.toString) +
@@ -141,20 +141,18 @@
     private def get_entry(row: Int): Option[Table_Entry] =
       if (0 <= row && row <= entries_count) Some(entries(row)) else None
 
-    private val ignored = Synchronized(Set.empty[Shortcut])
+    private val selected =
+      Synchronized[Set[Int]](
+        (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
 
     def select(row: Int, b: Boolean)
     {
-      for (entry <- get_entry(row) if entry.head) {
-        ignored.change(set => if (b) set - entry.shortcut else set + entry.shortcut)
-      }
+      if (get_entry(row).isDefined)
+        selected.change(set => if (b) set + row else set - row)
     }
 
     def selected_status(row: Int): Option[Boolean] =
-      get_entry(row) match {
-        case Some(entry) if entry.head => Some(!ignored.value.contains(entry.shortcut))
-        case _ => None
-      }
+      if (get_entry(row).isDefined) Some(selected.value.contains(row)) else None
 
     override def getColumnCount: Int = 2
 
@@ -182,15 +180,20 @@
 
     override def isCellEditable(row: Int, column: Int): Boolean =
       get_entry(row) match {
-        case Some(entry) => entry.head && column == 0
+        case Some(entry) => column == 0
         case None => false
       }
 
     override def setValueAt(value: AnyRef, row: Int, column: Int)
     {
       (get_entry(row), value) match {
-        case (Some(entry), b: java.lang.Boolean) if entry.head && column == 0 =>
-          select(row, b.booleanValue)
+        case (Some(entry), obj: java.lang.Boolean) if entry.head.isEmpty && column == 0 =>
+          val b = obj.booleanValue
+          select(row, b)
+          if (entry.tail.nonEmpty) {
+            entry.tail.foreach(select(_, !b))
+            GUI_Thread.later { fireTableDataChanged() }
+          }
         case _ =>
       }
     }
@@ -220,8 +223,11 @@
 
     val table_entries =
       for {
-        (shortcut, conflicts) <- shortcut_conflicts
-        entry <- Table_Entry(shortcut, true) :: conflicts.map(Table_Entry(_, false))
+        ((shortcut, conflicts), i) <- shortcut_conflicts zip
+          shortcut_conflicts.scanLeft(0)({ case (i, (_, conflicts)) => i + 1 + conflicts.length })
+        entry <-
+          Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) ::
+          conflicts.map(Table_Entry(_, Some(i), Nil))
       } yield entry
 
     val table_model = new Table_Model(table_entries)