# HG changeset patch
# User wenzelm
# Date 1745353308 -7200
# Node ID 26564f433980f58fab906e263e68c9e27b93f2ff
# Parent  7fac6b070a49b1bd7d60223550adc71cf5e408cf
tuned signature, following 1033ed5d3972;

diff -r 7fac6b070a49 -r 26564f433980 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 22:20:30 2025 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 22:21:48 2025 +0200
@@ -17,7 +17,8 @@
 
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
+  Gutter}
 
 
 object Document_View {
@@ -144,8 +145,7 @@
         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_left = gutter_insets.left + Gutter.FOLD_MARKER_SIZE
         val skip_right = gutter_insets.right
         val icon_width = gutter_width - skip_left - skip_right
         val icon_height = line_height