# HG changeset patch
# User wenzelm
# Date 1744842553 -7200
# Node ID 42ea1a06e56ee4f6fa313428a3113cc642d4bc61
# Parent  f67ad2dbf6d5834310600d8ec5ee60762f5b5d19
updated to jedit-20250417;
removed obsolete idea-icons-20250415: already bundled in jedit component;
clarified JEdit_Lib.load_icon, following afa1c2d485ae and 6d5a169c3a22;

diff -r f67ad2dbf6d5 -r 42ea1a06e56e Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Apr 17 00:25:58 2025 +0200
+++ b/Admin/components/components.sha1	Thu Apr 17 00:29:13 2025 +0200
@@ -270,6 +270,7 @@
 1aa375149dc5e84cfdd64bf66e7e0f68319b7db7 jedit-20250402.tar.gz
 88c9cc14f5618ad21ca17664fdb57b8f5f6f6d2e jedit-20250404.tar.gz
 cab6dca89dc2e0d922e92cc47df07941a3c6b29c jedit-20250415.tar.gz
+23297ab36a853247a17f87b94a29654f3259b341 jedit-20250417.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r f67ad2dbf6d5 -r 42ea1a06e56e Admin/components/main
--- a/Admin/components/main	Thu Apr 17 00:25:58 2025 +0200
+++ b/Admin/components/main	Thu Apr 17 00:29:13 2025 +0200
@@ -11,12 +11,11 @@
 find_facts_web-20250223
 flatlaf-3.6-1
 foiltex-2.1.4b
-idea-icons-20250415
 isabelle_fonts-20241227
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250415
+jedit-20250417
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3
diff -r f67ad2dbf6d5 -r 42ea1a06e56e src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 17 00:25:58 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 17 00:29:13 2025 +0200
@@ -13,7 +13,7 @@
 import java.awt.{Component, Container, Toolkit}
 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
 import java.awt.font.FontRenderContext
-import javax.swing.{Icon, ImageIcon, JScrollBar, JWindow}
+import javax.swing.{ImageIcon, JScrollBar, JWindow}
 
 import scala.util.parsing.input.CharSequenceReader
 import scala.util.matching.Regex
@@ -386,38 +386,8 @@
 
   /* icons */
 
-  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 match {
-        case svg_icon: FlatSVGIcon if scale != 1.0 => svg_icon.derive(scale.toFloat)
-        case _ => icon
-      }
-    }
-  }
-
-  def load_image_icon(name: String): ImageIcon =
-    load_icon(name) match {
-      case icon: ImageIcon => icon
-      case _ => error("Bad image icon: " + name)
-    }
+  def load_icon(spec: String): ImageIcon =
+    GUIUtilities.loadIcon(spec).asInstanceOf[ImageIcon]
 
 
   /* buffer event handling */
diff -r f67ad2dbf6d5 -r 42ea1a06e56e src/Tools/jEdit/src/process_indicator.scala
--- a/src/Tools/jEdit/src/process_indicator.scala	Thu Apr 17 00:25:58 2025 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala	Thu Apr 17 00:29:13 2025 +0200
@@ -18,10 +18,10 @@
   private val label = new Label
 
   private val passive_icon =
-    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
+    JEdit_Lib.load_icon(PIDE.options.string("process_passive_icon")).getImage
   private val active_icons =
     space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
-      JEdit_Lib.load_image_icon(name).getImage)
+      JEdit_Lib.load_icon(name).getImage)
 
   private class Animation extends ImageIcon(passive_icon) {
     private var current_frame = 0