update idea-icons: prefer scalable SVG;

--- a/Admin/components/components.sha1	Tue Apr 15 21:32:50 2025 +0200
+++ b/Admin/components/components.sha1	Tue Apr 15 23:38:33 2025 +0200
@@ -139,6 +139,7 @@
 964fb17e87f7a7e8a91895a696f7d059164ae742 hugo-0.142.0.tar.gz
 511fa8df8be88eb0500032bbd17742d33bdd4636 hugo-0.88.1.tar.gz
 989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz
+d7f72e7ef6e24ddf3b0d433d35b68658cabd1d88 idea-icons-20250415.tar.gz
 20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
 736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz
 9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz

--- a/Admin/components/main	Tue Apr 15 21:32:50 2025 +0200
+++ b/Admin/components/main	Tue Apr 15 23:38:33 2025 +0200
@@ -11,7 +11,7 @@
 find_facts_web-20250223
 flatlaf-3.6-1
 foiltex-2.1.4b
-idea-icons-20210508
+idea-icons-20250415
 isabelle_fonts-20241227
 isabelle_setup-20240327
 javamail-20250122

--- a/src/Tools/jEdit/etc/options	Tue Apr 15 21:32:50 2025 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Apr 15 23:38:33 2025 +0200
@@ -159,11 +159,11 @@
 
 section "Icons"
 
-option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
-option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
-option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
-option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
-option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
-option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
-option process_passive_icon : string = "idea-icons/process/step_passive.png"
-option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png"
+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 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/jedit_lib.scala	Tue Apr 15 21:32:50 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 23:38:33 2025 +0200
@@ -26,6 +26,8 @@
 import org.gjt.sp.jedit.buffer.{BufferListener, BufferAdapter, JEditBuffer, LineManager}
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection, AntiAlias}
 
+import com.formdev.flatlaf.extras.FlatSVGIcon
+
 
 object JEdit_Lib {
   /* jEdit directories */
@@ -384,16 +386,31 @@
 
   /* icons */
 
-  def load_icon(name: String): Icon = {
+  private val Icon_Spec = """^([^?]+)\?scale=(.+)$""".r
+
+  def load_icon(spec: String): Icon = {
+    val (name, scale) =
+      spec match {
+        case Icon_Spec(a, b) if Value.Double.unapply(b).isDefined =>
+          (a, Value.Double.parse(b))
+        case _ => (spec, 1.0)
+      }
+
     val name1 =
       if (name.startsWith("idea-icons/")) {
         val file = File.uri(Path.explode("$ISABELLE_IDEA_ICONS")).toASCIIString
         "jar:" + file + "!/" + name
       }
       else name
+
     val icon = GUIUtilities.loadIcon(name1)
     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
-    else icon
+    else {
+      icon match {
+        case svg_icon: FlatSVGIcon if scale != 1.0 => svg_icon.derive(scale.toFloat)
+        case _ => icon
+      }
+    }
   }
 
   def load_image_icon(name: String): ImageIcon =