--- 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"
--- 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 {