# HG changeset patch
# User wenzelm
# Date 1745348210 -7200
# Node ID f1b40256a45e9c6a3630c16c0c7792184f40664e
# Parent  99707a0a98d17ec279ff57d1c5bc44979df21914
clarified GUI calculations for icons;

diff -r 99707a0a98d1 -r f1b40256a45e src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 19:49:31 2025 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 20:56:50 2025 +0200
@@ -140,13 +140,18 @@
         GUI_Thread.assert {}
 
         val gutter = text_area.getGutter
-        val sel_width = GutterOptionPane.getSelectionAreaWidth
-        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
-        val FOLD_MARKER_SIZE = 12
+        val gutter_width = gutter.getWidth
+        val gutter_insets = gutter.getBorder.getBorderInsets(gutter)
+
+        // org.gjt.sp.jedit.textarea.Gutter.FOLD_MARKER_SIZE = 12
+        val skip_left = gutter_insets.left + 12
+        val skip_right = gutter_insets.right
+        val icon_width = gutter_width - skip_left - skip_right
+        val icon_height = line_height
 
         val gutter_icons =
           !gutter.isExpanded &&
-            gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12
+            gutter.isSelectionAreaEnabled && icon_width >= 12 && icon_height >= 12
 
         val buffer = model.buffer
         JEdit_Lib.buffer_lock(buffer) {
@@ -162,15 +167,15 @@
                   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)
+                    val x0 = skip_left + (((icon_width - w) / 2) max 0)
+                    val y0 = y + i * line_height + (((icon_height - h) / 2) max 0)
                     icon.paintIcon(gutter, gfx, x0, y0)
                   }
                   // background only
                   else {
                     val y0 = y + i * line_height
                     gfx.setColor(color)
-                    gfx.fillRect(0, y0, gutter.getWidth, line_height)
+                    gfx.fillRect(0, y0, gutter_width, line_height)
                   }
                 case None =>
               }