tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);

--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 04 14:10:21 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 04 14:39:27 2024 +0100
@@ -334,7 +334,7 @@
             // line background color
             for { (c, separator) <- rendering.line_background(line_range) } {
               gfx.setColor(rendering.color(c))
-              val sep = if (separator) 2 min (line_height / 2) else 0
+              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)
             }