# HG changeset patch
# User wenzelm
# Date 1745344171 -7200
# Node ID 99707a0a98d17ec279ff57d1c5bc44979df21914
# Parent  ea65da20d173bab8cdcfdea62ddc71754962c25a
tuned;

diff -r ea65da20d173 -r 99707a0a98d1 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 17:49:56 2025 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 19:49:31 2025 +0200
@@ -144,6 +144,10 @@
         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
         val FOLD_MARKER_SIZE = 12
 
+        val gutter_icons =
+          !gutter.isExpanded &&
+            gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12
+
         val buffer = model.buffer
         JEdit_Lib.buffer_lock(buffer) {
           val rendering = Document_View.rendering(doc_view)
@@ -155,15 +159,14 @@
               rendering.gutter_content(line_range) match {
                 case Some((icon, color)) =>
                   // icons within selection area
-                  if (!gutter.isExpanded &&
-                      gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12) {
-                    val x0 =
-                      (FOLD_MARKER_SIZE + sel_width - border_width - icon.getIconWidth) max 10
-                    val y0 =
-                      y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
+                  if (gutter_icons) {
+                    val w = icon.getIconWidth
+                    val h = icon.getIconHeight
+                    val x0 = (FOLD_MARKER_SIZE + sel_width - border_width - w) max 10
+                    val y0 = y + i * line_height + (((line_height - h) / 2) max 0)
                     icon.paintIcon(gutter, gfx, x0, y0)
                   }
-                  // background
+                  // background only
                   else {
                     val y0 = y + i * line_height
                     gfx.setColor(color)