# HG changeset patch # User wenzelm # Date 1735316811 -3600 # Node ID 09c16e5636ad900ca81440fc433badab2c6a9121 # Parent ca4ecbbdd7282350a5372417fd046b4e0473d27c tuned generated output: more standard operations; diff -r ca4ecbbdd728 -r 09c16e5636ad src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala Fri Dec 27 17:26:01 2024 +0100 +++ b/src/Tools/jEdit/src/keymap_merge.scala Fri Dec 27 17:26:51 2024 +0100 @@ -102,12 +102,14 @@ PIDE.options.color_value("error_color") private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) { - override def toString: String = - if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" - else - "" + - HTML.output("--- " + shortcut.toString) + - "" + override def toString: String = { + val style = GUI.Style_HTML + if (head.isEmpty) style.enclose(style.make_text(shortcut.toString)) + else { + style.enclose_style(HTML.color_property(conflict_color), + style.make_text("--- " + shortcut.toString)) + } + } } private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel {