# HG changeset patch # User wenzelm # Date 1472668515 -7200 # Node ID 352a257fa13a4e96096dbfc4f83a49ed21b93827 # Parent f215f5f5bd35c1f13a6026a5322f14db7b47e3ca tuned GUI; diff -r f215f5f5bd35 -r 352a257fa13a src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala Wed Aug 31 18:33:42 2016 +0200 +++ b/src/Tools/jEdit/src/keymap_merge.scala Wed Aug 31 20:35:15 2016 +0200 @@ -10,7 +10,7 @@ import isabelle._ import java.lang.Class -import java.awt.Dimension +import java.awt.{Color, Dimension} import java.awt.event.WindowEvent import javax.swing.{WindowConstants, JDialog, JTable, JScrollPane} import javax.swing.table.AbstractTableModel @@ -122,13 +122,16 @@ /** table model **/ + private def conflict_color: Color = + PIDE.options.color_value("error_color") + private sealed case class Table_Entry(shortcut: Shortcut, head: Boolean) { override def toString: String = if (head) "" + HTML.output(shortcut.toString) + "" else - "" + - HTML.output(" -- " + shortcut.toString) + + "" + + HTML.output("--- " + shortcut.toString) + "" } @@ -170,13 +173,27 @@ case Some(entry) if column == 0 => selected_status(row) match { case None => null - case Some(true) => java.lang.Boolean.TRUE - case Some(false) => java.lang.Boolean.FALSE + case Some(b) => java.lang.Boolean.valueOf(b) } case Some(entry) if column == 1 => entry case _ => null } } + + override def isCellEditable(row: Int, column: Int): Boolean = + get_entry(row) match { + case Some(entry) => entry.head && 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 _ => + } + } }