# HG changeset patch # User wenzelm # Date 1731081126 -3600 # Node ID 7acc6fabca6adb6ec00f0ac71d77c3a501321b6d # Parent 5f401c2f7d333dbad3424df9be88f27b0ea33068 clarified signature; diff -r 5f401c2f7d33 -r 7acc6fabca6a src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 15:08:36 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 16:52:06 2024 +0100 @@ -356,23 +356,16 @@ def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(JEdit_Rendering.squiggly_elements, range) - def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] = { - val results = - snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ => - { - case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) - }) - val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 } + def line_background(range: Text.Range): Option[Rendering.Color.Value] = + Rendering.message_background_color.get( + snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ => { + case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) + }).foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 }) - Rendering.message_background_color.get(pri).map(message_color => { - val is_separator = - snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ => - { - case _ => Some(true) - }).exists(_.info) - (message_color, is_separator) - }) - } + def line_separator(range: Text.Range): Boolean = + snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ => { + case _ => Some(true) + }).exists(_.info) /* text color */ diff -r 5f401c2f7d33 -r 7acc6fabca6a src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 08 15:08:36 2024 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 08 16:52:06 2024 +0100 @@ -332,9 +332,10 @@ val line_range = Text.Range(start(i), end(i) min buffer.getLength) // line background color - for { (c, separator) <- rendering.line_background(line_range) } { + for (c <- rendering.line_background(line_range)) { + val separator = rendering.line_separator(line_range) + val sep = if (separator) (2 min (line_height / 2)) max (line_height / 8) else 0 gfx.setColor(rendering.color(c)) - val sep = if (separator) (2 min (line_height / 2)) max (line_height / 8) else 0 gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) }