# 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)
             }