# HG changeset patch # User wenzelm # Date 1472661222 -7200 # Node ID f215f5f5bd35c1f13a6026a5322f14db7b47e3ca # Parent 6de6e883c5fb65dc395c80ddde4c083f4055ebd0 tuned rendering; diff -r 6de6e883c5fb -r f215f5f5bd35 src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala Wed Aug 31 18:15:32 2016 +0200 +++ b/src/Tools/jEdit/src/keymap_merge.scala Wed Aug 31 18:33:42 2016 +0200 @@ -124,7 +124,12 @@ private sealed case class Table_Entry(shortcut: Shortcut, head: Boolean) { - override def toString: String = shortcut.toString + override def toString: String = + if (head) "" + HTML.output(shortcut.toString) + "" + else + "" + + HTML.output(" -- " + shortcut.toString) + + "" } private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel @@ -168,7 +173,7 @@ case Some(true) => java.lang.Boolean.TRUE case Some(false) => java.lang.Boolean.FALSE } - case Some(entry) if column == 1 => entry.shortcut + case Some(entry) if column == 1 => entry case _ => null } }