# HG changeset patch # User wenzelm # Date 1472671554 -7200 # Node ID 7b2963b11e4a7d8b288385bc1ab2e4c471522047 # Parent 352a257fa13a4e96096dbfc4f83a49ed21b93827 clarified GUI; diff -r 352a257fa13a -r 7b2963b11e4a 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.output(shortcut.toString) + "" + if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" else "" + 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)