# HG changeset patch
# User wenzelm
# Date 1745350223 -7200
# Node ID d4c1f7d0fcc658437c5a8e21a787fe22bd9c2e11
# Parent  f1b40256a45e9c6a3630c16c0c7792184f40664e
more accurate GUI painting;

diff -r f1b40256a45e -r d4c1f7d0fcc6 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Apr 22 20:56:50 2025 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Apr 22 21:30:23 2025 +0200
@@ -161,9 +161,9 @@
 
 option tooltip_close_icon : string = "idea-icons/actions/closeDarkGrey.svg"
 option tooltip_detach_icon : string = "idea-icons/actions/copy.svg"
-option gutter_information_icon : string = "idea-icons/general/information.svg?scale=0.65"
-option gutter_warning_icon : string = "idea-icons/general/warning.svg?scale=0.65"
-option gutter_legacy_icon : string = "idea-icons/runConfigurations/testFailed.svg?scale=0.65"
-option gutter_error_icon : string = "idea-icons/general/error.svg?scale=0.65"
+option gutter_information_icon : string = "idea-icons/general/information.svg"
+option gutter_warning_icon : string = "idea-icons/general/warning.svg"
+option gutter_legacy_icon : string = "idea-icons/runConfigurations/testFailed.svg"
+option gutter_error_icon : string = "idea-icons/general/error.svg"
 option process_passive_icon : string = "idea-icons/process/big/step_passive.svg?scale=0.5"
 option process_active_icons : string = "idea-icons/process/big/step_1.svg?scale=0.5:idea-icons/process/big/step_2.svg?scale=0.5:idea-icons/process/big/step_3.svg?scale=0.5:idea-icons/process/big/step_4.svg?scale=0.5:idea-icons/process/big/step_5.svg?scale=0.5:idea-icons/process/big/step_6.svg?scale=0.5:idea-icons/process/big/step_7.svg?scale=0.5:idea-icons/process/big/step_8.svg?scale=0.5"
diff -r f1b40256a45e -r d4c1f7d0fcc6 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 20:56:50 2025 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 21:30:23 2025 +0200
@@ -12,6 +12,7 @@
 
 import java.awt.Graphics2D
 import java.awt.event.KeyEvent
+import java.awt.geom.AffineTransform
 import javax.swing.event.{CaretListener, CaretEvent}
 
 import org.gjt.sp.jedit.jEdit
@@ -149,6 +150,8 @@
         val icon_width = gutter_width - skip_left - skip_right
         val icon_height = line_height
 
+        def scale(a: Int, b: Int): Double = 0.95 * a.toDouble / b.toDouble
+
         val gutter_icons =
           !gutter.isExpanded &&
             gutter.isSelectionAreaEnabled && icon_width >= 12 && icon_height >= 12
@@ -164,12 +167,21 @@
               rendering.gutter_content(line_range) match {
                 case Some((icon, color)) =>
                   // icons within selection area
-                  if (gutter_icons) {
-                    val w = icon.getIconWidth
-                    val h = icon.getIconHeight
+                  if (gutter_icons && icon.getIconWidth > 0 && icon.getIconHeight > 0) {
+                    val w0 = icon.getIconWidth
+                    val h0 = icon.getIconHeight
+                    val s = Math.min(scale(icon_width, w0), scale(icon_height, h0))
+
+                    val w = (s * w0).ceil
+                    val h = (s * h0).ceil
                     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)
+
+                    val tr0 = gfx.getTransform
+                    val tr = new AffineTransform(tr0); tr.translate(x0, y0); tr.scale(s, s)
+                    gfx.setTransform(tr)
+                    icon.paintIcon(gutter, gfx, 0, 0)
+                    gfx.setTransform(tr0)
                   }
                   // background only
                   else {