# HG changeset patch
# User wenzelm
# Date 1745420329 -7200
# Node ID 9390f8e3b1c172d5d76f62098d15a8f0d1fc91e7
# Parent  32a6228f543d89b45c5e4d15def8f76abfe1c03f# Parent  9720ebc51bcbbdfca20a01f0c3978285e608e669
merged

diff -r 32a6228f543d -r 9390f8e3b1c1 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Apr 23 14:42:38 2025 +0200
+++ b/Admin/components/components.sha1	Wed Apr 23 16:58:49 2025 +0200
@@ -129,6 +129,9 @@
 31d6abd58a4c2f7522f14283dfe04e2801a6e828 flatlaf-2.6.tar.gz
 95aff7a320715c473ea63294a288ba30a71dec88 flatlaf-3.5.4-1.tar.gz
 a93a98c80536a6984db118e129b1b3a778c700ce flatlaf-3.5.4.tar.gz
+7de5b13afd4d9ac09e4d591b63c1979b9276e4f6 flatlaf-3.6-1.tar.gz
+372ac19c1783af818591c379e1646a3fc1fbbfc2 flatlaf-3.6-2.tar.gz
+1363421c87dd24bbff318e37c4788ba0339db7ad flatlaf-3.6.tar.gz
 b1c40ce6c087da7e70e221ddd3fcadfa569acb2f foiltex-2.1.4b.tar.gz
 f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
 71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz
@@ -137,6 +140,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
@@ -266,6 +270,10 @@
 12f22ccb48a0a7dc9ad8c1b27552e8fd26d4ae0c jedit-20250215.tar.gz
 1aa375149dc5e84cfdd64bf66e7e0f68319b7db7 jedit-20250402.tar.gz
 88c9cc14f5618ad21ca17664fdb57b8f5f6f6d2e jedit-20250404.tar.gz
+cab6dca89dc2e0d922e92cc47df07941a3c6b29c jedit-20250415.tar.gz
+23297ab36a853247a17f87b94a29654f3259b341 jedit-20250417.tar.gz
+a291746959e64916e8504b89dca804186d4eb8a1 jedit-20250422.tar.gz
+07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
@@ -322,6 +330,7 @@
 df8bb213d39a7eecae97e6af3b11752d6c704c90 jsoup-1.15.4.tar.gz
 b1c8e2a289e40cbc139a3c371348cef3b537b1c7 jsoup-1.17.2.tar.gz
 342f12a07889ec173b13df9327db684b45118252 jsoup-1.18.3.tar.gz
+a7419f9dab68e50d05533980b6729d1dd7aafb3b jsvg-1.7.1.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
 afb04f4048a87bb888fe7b05b0139cb060c7925b kodkodi-1.5.2-1.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
diff -r 32a6228f543d -r 9390f8e3b1c1 Admin/components/main
--- a/Admin/components/main	Wed Apr 23 14:42:38 2025 +0200
+++ b/Admin/components/main	Wed Apr 23 16:58:49 2025 +0200
@@ -9,17 +9,17 @@
 easychair-3.5
 eptcs-1.7.0
 find_facts_web-20250223
-flatlaf-3.5.4-1
+flatlaf-3.6-2
 foiltex-2.1.4b
-idea-icons-20210508
 isabelle_fonts-20241227
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250404
+jedit-20250423
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3
+jsvg-1.7.1
 kodkodi-1.5.7
 lipics-3.1.3
 llncs-2.25
diff -r 32a6228f543d -r 9390f8e3b1c1 NEWS
--- a/NEWS	Wed Apr 23 14:42:38 2025 +0200
+++ b/NEWS	Wed Apr 23 16:58:49 2025 +0200
@@ -37,6 +37,27 @@
 longer included. The old-fashioned toolbar, with its old Navigator
 icons, is now disabled by default.
 
+* Update GUI look-and-feel to current FlatLaf 3.6, with native library
+support on all Isabelle platforms (now including arm64-linux).
+
+* Additional look-and-feels "FlatLaf macOS Light" and "FlatLaf macOS
+Dark" imitate original macOS more closely. This is the default for the
+bundled application on macOS.
+
+* GUI rendering of the gutter is now more accurate, using scaled icons
+to fit precisely into the available space.
+
+* GUI rendering for dark look-and-feels has been slightly improved, e.g.
+menu accelerator font/color.
+
+* Provide scalable icons for old-fashioned "tango" (from early Gnome or
+KDE), and "idea-icons" from current IntelliJ IDEA community edition. All
+icons are available for jEdit and Isabelle/jEdit add-ons. The special
+notation "myicon.svg?scale=0.5" allows to resize icons as specified in
+jEdit properties. The default properties of Isabelle/jEdit usually
+prefer scalable icons over fixed old bitmaps, but some notable icons are
+not available as SVG.
+
 
 *** HOL ***
 
@@ -191,6 +212,10 @@
 * SSH connections allow both bash and zsh as remote shell. This is
 particularly important for macOS, where zsh is the default user shell.
 
+* Isabelle/Scala supports SVG via the "jsvg" library
+(com.github.weisj.jsvg.SVGDocument), as well as the "flatlaf-extras"
+library (com.formdev.flatlaf.extras.FlatSVGIcon).
+
 
 
 New in Isabelle2025 (March 2025)
diff -r 32a6228f543d -r 9390f8e3b1c1 etc/build.props
--- a/etc/build.props	Wed Apr 23 14:42:38 2025 +0200
+++ b/etc/build.props	Wed Apr 23 16:58:49 2025 +0200
@@ -36,6 +36,7 @@
   src/Pure/Admin/component_jdk.scala \
   src/Pure/Admin/component_jedit.scala \
   src/Pure/Admin/component_jsoup.scala \
+  src/Pure/Admin/component_jsvg.scala \
   src/Pure/Admin/component_lipics.scala \
   src/Pure/Admin/component_llncs.scala \
   src/Pure/Admin/component_minisat.scala \
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -691,7 +691,8 @@
 
           case Platform.Family.macos =>
             File.change(isabelle_target + jedit_props) {
-              _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+              _.replaceAll("lookAndFeel=.*", "lookAndFeel=com.formdev.flatlaf.themes.FlatMacLightLaf")
+               .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
                .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
             }
 
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/Admin/component_flatlaf.scala
--- a/src/Pure/Admin/component_flatlaf.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/Admin/component_flatlaf.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -8,22 +8,31 @@
 
 
 object Component_FlatLaf {
-  /* platform information */
+  /* jars and native libraries */
 
-  sealed case class Platform_Info(name: String, exe: Boolean = false)
+  sealed case class Lib(template: String, exe: Boolean = false) {
+    def path(version: String): Path =
+      Path.explode(template.replace("{V}", version))
+
+    def jar_name(version: String): Option[String] =
+      if (File.is_jar(template)) Some(path(version).file_name) else None
+  }
 
-  private val platforms =
+  private val libs =
     List(
-      Platform_Info("flatlaf-{V}-macos-arm64.dylib"),
-      Platform_Info("flatlaf-{V}-macos-x86_64.dylib"),
-      Platform_Info("flatlaf-{V}-linux-x86_64.so"),
-      Platform_Info("flatlaf-{V}-windows-x86_64.dll", exe = true))
+      Lib("flatlaf/{V}/flatlaf-{V}-no-natives.jar"),
+      Lib("flatlaf/{V}/flatlaf-{V}-macos-arm64.dylib"),
+      Lib("flatlaf/{V}/flatlaf-{V}-macos-x86_64.dylib"),
+      Lib("flatlaf/{V}/flatlaf-{V}-linux-arm64.so"),
+      Lib("flatlaf/{V}/flatlaf-{V}-linux-x86_64.so"),
+      Lib("flatlaf/{V}/flatlaf-{V}-windows-x86_64.dll", exe = true),
+      Lib("flatlaf-extras/{V}/flatlaf-extras-{V}.jar"))
 
 
   /* build flatlaf */
 
-  val default_download_url = "https://repo1.maven.org/maven2/com/formdev/flatlaf"
-  val default_version = "3.5.4"
+  val default_download_url = "https://repo1.maven.org/maven2/com/formdev"
+  val default_version = "3.6"
 
   def build_flatlaf(
     target_dir: Path = Path.current,
@@ -42,28 +51,32 @@
 
     Isabelle_System.make_directory(component_dir.lib)
 
-    def download(name: String, exe: Boolean = false): Unit = {
-      val download_name = name.replace("{V}", version)
-      val target = component_dir.lib + Path.basic(download_name)
+    for (lib <- libs) {
+      val lib_path = lib.path(version)
+      val target = component_dir.lib + Path.basic(lib_path.file_name)
       Isabelle_System.download_file(
-        download_url + "/" + version + "/" + download_name, target, progress = progress)
-      if (exe) File.set_executable(target)
+        download_url + "/" + lib_path.implode, target, progress = progress)
+      if (lib.exe) File.set_executable(target)
     }
 
-    download("flatlaf-{V}-no-natives.jar")
-
-    for (platform <- platforms) download(platform.name, exe = platform.exe)
+    val jar_names = libs.flatMap(_.jar_name(version))
 
 
     /* settings */
 
+    val classpath =
+      libs.flatMap(_.jar_name(version)).map(a => "$ISABELLE_FLATLAF_HOME/lib/" + a)
+        .mkString(":")
+
     component_dir.write_settings("""
 ISABELLE_FLATLAF_HOME="$COMPONENT"
 
-classpath "$ISABELLE_FLATLAF_HOME/lib/flatlaf-""" + version + """-no-natives.jar"
+classpath """ + quote(classpath) + """
 
 isabelle_scala_service "isabelle.FlatLightLaf"
 isabelle_scala_service "isabelle.FlatDarkLaf"
+isabelle_scala_service "isabelle.FlatMacLightLaf"
+isabelle_scala_service "isabelle.FlatMacDarkLaf"
 """)
 
 
@@ -71,11 +84,14 @@
 
     File.write(component_dir.README,
       """This is the FlatLaf Java/Swing look-and-feel from
-https://www.formdev.com/flatlaf and
-https://mvnrepository.com/artifact/com.formdev/flatlaf
+https://mvnrepository.com/artifact/com.formdev
 
 It is covered by the Apache License 2.0 license.
 
+See also https://www.formdev.com/flatlaf  and especially the demo
+application https://download.formdev.com/flatlaf/flatlaf-demo-latest.jar
+(which may be run via "java -jar ...").
+
 
         Makarius
         """ + Date.Format.date(Date.now()) + "\n")
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -144,6 +144,24 @@
       Isabelle_System.extract(source_path, jedit_dir)
 
 
+      /* tango icons (SVG) */
+
+      val tango_path = Isabelle_System.make_directory(tmp_dir + Path.explode("tango"))
+      Isabelle_System.download_file(
+        "https://github.com/stephenc/tango-icon-theme/archive/41b8f6abd7eb.zip",
+        tango_path.zip, progress = progress)
+      Isabelle_System.extract(tango_path.zip, tango_path, strip = true)
+
+
+      /* IntelliJ IDEA icons (SVG) */
+
+      val idea_path = Isabelle_System.make_directory(tmp_dir + Path.explode("idea"))
+      Isabelle_System.download_file(
+        "https://isabelle.sketis.net/components/idea-icons-20250415.tar.gz",
+        idea_path.tar.gz, progress = progress)
+      Isabelle_System.extract(idea_path.tar.gz, idea_path, strip = true)
+
+
       /* patched version */
 
       Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
@@ -161,12 +179,30 @@
           cwd = source_dir, echo = true).check
       }
 
-      for { theme <- List("classic", "tango") } {
-        val path = Path.explode("org/gjt/sp/jedit/icons/themes/" + theme + "/32x32/apps/isabelle.gif")
+      progress.echo("Augmenting icons ...")
+
+      val jedit_icons_path = source_dir + Path.explode("org/gjt/sp/jedit/icons/themes")
+      val jedit_classic_path = jedit_icons_path + Path.basic("classic")
+      val jedit_tango_path = jedit_icons_path + Path.basic("tango")
+      val jedit_idea_path = jedit_tango_path + Path.basic("idea-icons")
+
+      for (theme <- List(jedit_classic_path, jedit_tango_path)) {
         Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle_transparent-32.gif"),
-          source_dir + path)
+          theme + Path.explode("32x32/apps/isabelle.gif"))
       }
 
+      for {
+        svg_file <- File.find_files(tango_path.file, pred = file => File.is_svg(file.getName))
+        rel_path <- File.relative_path(tango_path, File.path(svg_file))
+      } {
+        val dir = Isabelle_System.make_directory(jedit_tango_path + rel_path.dir)
+        Isabelle_System.copy_file(File.path(svg_file), dir + rel_path.base)
+      }
+
+      Isabelle_System.extract(idea_path + Path.explode("jar/idea-icons.jar"), jedit_tango_path)
+      Isabelle_System.rm_tree(jedit_tango_path + Path.explode("META-INF"))
+      Isabelle_System.copy_file(idea_path + Path.explode("README"), jedit_idea_path)
+
       progress.echo("Building jEdit ...")
       Isabelle_System.copy_dir(source_dir, tmp_source_dir)
       progress.bash("ant", cwd = tmp_source_dir, echo = true).check
@@ -340,10 +376,8 @@
 metal.secondary.fontsize=12
 navigate-backwards.label=Navigate backwards
 navigate-backwards.shortcut=AS+LEFT
-navigate-backwards.icon=ArrowL.png
 navigate-forwards.label=Navigate forwards
 navigate-forwards.shortcut=AS+RIGHT
-navigate-forwards.icon=ArrowR.png
 navigate-toolbar=navigate-backwards navigate-forwards
 navigator.showOnToolbar=true
 new-file-in-mode.shortcut=
@@ -363,7 +397,6 @@
 recent-buffer.shortcut2=C+CIRCUMFLEX
 restore.remote=false
 restore=false
-search.find=Search:
 search.subdirs.toggle=true
 select-block.shortcut2=C+8
 sidekick-tree.dock-position=right
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/Admin/component_jsvg.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_jsvg.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -0,0 +1,92 @@
+/*  Title:      Pure/Admin/component_jsvg.scala
+    Author:     Makarius
+
+Build Isabelle jsvg component from official download.
+*/
+
+package isabelle
+
+
+object Component_JSVG {
+  /* build jsvg */
+
+  val default_download_url =
+    "https://repo1.maven.org/maven2/com/github/weisj/jsvg/1.7.1/jsvg-1.7.1.jar"
+
+  def build_jsvg(
+    download_url: String = default_download_url,
+    progress: Progress = new Progress,
+    target_dir: Path = Path.current
+  ): Unit = {
+    val Download_Name = """^.*/([^/]+)\.jar""".r
+    val download_name =
+      download_url match {
+        case Download_Name(download_name) => download_name
+        case _ => error("Malformed jar download URL: " + quote(download_url))
+      }
+
+
+    /* component */
+
+    val component_dir =
+      Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
+
+    File.write(component_dir.LICENSE,
+      Url.read("https://raw.githubusercontent.com/weisJ/jsvg/refs/heads/master/LICENSE"))
+
+
+    /* README */
+
+    File.write(component_dir.README,
+      "This is a Java SVG implementation (JSVG) from\n" + download_url +
+        "\n\nSee also https://github.com/weisJ/jsvg" +
+        "\n\n        Makarius\n        " + Date.Format.date(Date.now()) + "\n")
+
+
+    /* settings */
+
+    component_dir.write_settings("""
+ISABELLE_JSVG_HOME="$COMPONENT"
+
+classpath "$ISABELLE_JSVG_HOME/lib/""" + download_name + """.jar"
+""")
+
+
+    /* jar */
+
+    val jar = component_dir.lib + Path.basic(download_name).jar
+    Isabelle_System.make_directory(jar.dir)
+    Isabelle_System.download_file(download_url, jar, progress = progress)
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("component_jsvg", "build Isabelle jsvg component from official download",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var download_url = default_download_url
+
+        val getopts = Getopts("""
+Usage: isabelle component_jsvg [OPTIONS] DOWNLOAD
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL
+                 (default: """" + default_download_url + """")
+
+  Build jsvg component from the specified download URL (JAR).
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_jsvg(download_url = download_url, progress = progress, target_dir = target_dir)
+      })
+}
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/GUI/gui.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -18,21 +18,20 @@
 import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Separator}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
+import com.formdev.flatlaf
+import com.formdev.flatlaf.FlatLaf
+
 
 object GUI {
   /* Swing look-and-feel */
 
-  def init_laf(): Unit = {
-    val prop = com.formdev.flatlaf.FlatSystemProperties.USE_NATIVE_LIBRARY
-    System.setProperty(prop, System.getProperty(prop, "false"))
-    com.formdev.flatlaf.FlatLightLaf.setup()
-  }
-
   def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
 
-  def is_macos_laf: Boolean =
+  def is_macos_laf(): Boolean =
     Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
 
+  def is_dark_laf(): Boolean = FlatLaf.isLafDark()
+
   class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service {
     def info: UIManager.LookAndFeelInfo =
       new UIManager.LookAndFeelInfo(laf.getName, laf.getClass.getName)
@@ -56,6 +55,11 @@
     UIManager.put("Component.arrowType", "triangle")
   }
 
+  def init_laf(): Unit = {
+    init_lafs()
+    flatlaf.FlatLightLaf.setup()
+  }
+
 
   /* additional look-and-feels */
 
@@ -541,5 +545,7 @@
   }
 }
 
-class FlatLightLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatLightLaf)
-class FlatDarkLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatDarkLaf)
+class FlatLightLaf extends GUI.Look_And_Feel(new flatlaf.FlatLightLaf)
+class FlatDarkLaf extends GUI.Look_And_Feel(new flatlaf.FlatDarkLaf)
+class FlatMacLightLaf extends GUI.Look_And_Feel(new flatlaf.themes.FlatMacLightLaf)
+class FlatMacDarkLaf extends GUI.Look_And_Feel(new flatlaf.themes.FlatMacDarkLaf)
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/GUI/tree_view.scala
--- a/src/Pure/GUI/tree_view.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/GUI/tree_view.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -80,7 +80,7 @@
   }
 
   // follow jEdit
-  if (!GUI.is_macos_laf) {
+  if (!GUI.is_macos_laf()) {
     putClientProperty("JTree.lineStyle", "Angled")
   }
 }
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/General/file.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -102,6 +102,7 @@
   def is_pdf(s: String): Boolean = s.endsWith(".pdf")
   def is_png(s: String): Boolean = s.endsWith(".png")
   def is_scala(s: String): Boolean = s.endsWith(".scala")
+  def is_svg(s: String): Boolean = s.endsWith(".svg")
   def is_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2")
   def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
   def is_tar_xz(s: String): Boolean = s.endsWith(".tar.xz")
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/General/path.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -266,6 +266,7 @@
   def thy: Path = ext("thy")
   def xml: Path = ext("xml")
   def xz: Path = ext("xz")
+  def zip: Path = ext("zip")
   def zst: Path = ext("zst")
 
   def backup: Path = {
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -189,6 +189,7 @@
   Component_JDK.isabelle_tool,
   Component_JEdit.isabelle_tool,
   Component_Jsoup.isabelle_tool,
+  Component_JSVG.isabelle_tool,
   Component_LIPIcs.isabelle_tool,
   Component_LLNCS.isabelle_tool,
   Component_Minisat.isabelle_tool,
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Apr 23 16:58:49 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"
+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 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/gui_utilities
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/gui_utilities	Wed Apr 23 16:58:49 2025 +0200
@@ -0,0 +1,137 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2025-04-23 14:28:53.149349418 +0200
+@@ -42,6 +42,8 @@
+ import java.net.URL;
+ import java.util.*;
+ import java.util.List;
++import java.util.regex.Pattern;
++import java.util.regex.Matcher;
+ import java.lang.ref.SoftReference;
+ 
+ import javax.annotation.Nonnull;
+@@ -72,6 +74,8 @@
+ import java.util.concurrent.ScheduledExecutorService;
+ import java.util.concurrent.TimeUnit;
+ import java.util.concurrent.atomic.AtomicLong;
++
++import com.formdev.flatlaf.extras.FlatSVGIcon;
+ //}}}
+ 
+ /** Various GUI utility functions related to icons, menus, toolbars, keyboard shortcuts, etc.
+@@ -115,14 +119,14 @@
+ 	 * @return the icon
+ 	 * @since jEdit 2.6pre7
+ 	 */
+-	public static Icon loadIcon(String iconName)
++	public static Icon loadIcon(String iconSpec)
+ 	{
+-		if(iconName == null)
++		if(iconSpec == null)
+ 			return null;
+ 
+ 		// * Enable old icon naming scheme support
+-		if(deprecatedIcons.containsKey(iconName))
+-			iconName = deprecatedIcons.get(iconName);
++		if(deprecatedIcons.containsKey(iconSpec))
++			iconSpec = deprecatedIcons.get(iconSpec);
+ 
+ 		// check if there is a cached version first
+ 		Map<String, Icon> cache = null;
+@@ -135,12 +139,25 @@
+ 			cache = new HashMap<>();
+ 			iconCache = new SoftReference<>(cache);
+ 		}
+-		Icon icon = cache.get(iconName);
++		Icon icon = cache.get(iconSpec);
+ 		if(icon != null)
+ 			return icon;
+ 
+ 		URL url;
+ 
++		float iconScale = 1.0f;
++ 		String iconName = iconSpec;
++       {
++        	Matcher matcher = Pattern.compile("^([^?]+)\\?scale=(.+)$").matcher(iconSpec);
++        	if (matcher.matches()) {
++        		try {
++        			iconScale = Float.valueOf(matcher.group(2));
++        			iconName = matcher.group(1);
++        		}
++        		catch (NumberFormatException e) { }
++        	}
++        }
++
+ 		try
+ 		{
+ 			// get the icon
+@@ -164,9 +181,11 @@
+ 			}
+ 		}
+ 
+-		icon = new ImageIcon(url);
++		icon =
++			url.toString().endsWith(".svg") ?
++				new FlatSVGIcon(url).derive(iconScale) : new ImageIcon(url);
+ 
+-		cache.put(iconName,icon);
++		cache.put(iconSpec,icon);
+ 		return icon;
+ 	} //}}}
+ 
+@@ -1094,9 +1113,7 @@
+ 				return new Font("Monospaced", Font.PLAIN, 12);
+ 			}
+ 			else {
+-				Font font2 =
+-					new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
+-						Font.PLAIN, font1.getSize());
++				Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
+ 				FontRenderContext frc = new FontRenderContext(null, true, false);
+ 				float scale =
+ 					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
+@@ -1107,6 +1124,22 @@
+ 
+ 	//{{{ Colors and styles
+ 
++	public static Color menuAcceleratorForeground(boolean selection) {
++		Color color =
++			UIManager.getColor(selection ?
++				"MenuItem.acceleratorSelectionForeground" :
++				"MenuItem.acceleratorForeground");
++
++		if (color == null) color = Color.black;
++
++		return color;
++	}
++
++	public static boolean isDarkLaf()
++	{
++		return com.formdev.flatlaf.FlatLaf.isLafDark();
++	}
++
+ 	//{{{ getStyleString() method
+ 	/**
+ 	 * Converts a style into it's string representation.
+@@ -1619,6 +1652,21 @@
+ 	}
+ 	//}}}
+ 
++	//{{{ isPopupTrigger() method
++	/**
++	 * Returns if the specified event is the popup trigger event.
++	 * This implements precisely defined behavior, as opposed to
++	 * MouseEvent.isPopupTrigger().
++	 * @param evt The event
++	 * @since jEdit 3.2pre8
++	 * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
++	 */
++	@Deprecated
++	public static boolean isPopupTrigger(MouseEvent evt)
++	{
++		return GenericGUIUtilities.isPopupTrigger(evt);
++	} //}}}
++
+ 	//{{{ init() method
+ 	static void init()
+ 	{
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/gutter
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/gutter	Wed Apr 23 16:58:49 2025 +0200
@@ -0,0 +1,12 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/Gutter.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/Gutter.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/Gutter.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/Gutter.java	2025-04-22 22:08:05.106604316 +0200
+@@ -682,7 +682,7 @@
+ 	//{{{ Private members
+ 
+ 	//{{{ Instance variables
+-	private static final int FOLD_MARKER_SIZE = 12;
++	public static final int FOLD_MARKER_SIZE = 12;
+ 	private static final int SELECTION_GUTTER_WIDTH = 12;
+ 		// The selection gutter exists only if the gutter is not expanded
+ 
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/icons
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/icons	Wed Apr 23 16:58:49 2025 +0200
@@ -0,0 +1,580 @@
+diff -ru jedit5.7.0/jEdit/build.xml jedit5.7.0-patched/jEdit/build.xml
+--- jedit5.7.0/jEdit/build.xml	2024-08-03 19:53:28.000000000 +0200
++++ jedit5.7.0-patched/jEdit/build.xml	2025-04-16 17:20:57.401732024 +0200
+@@ -488,6 +488,7 @@
+ 				<include name="org/gjt/sp/jedit/icons/**/*.gif"/>
+ 				<include name="org/gjt/sp/jedit/icons/**/*.jpg"/>
+ 				<include name="org/gjt/sp/jedit/icons/**/*.png"/>
++				<include name="org/gjt/sp/jedit/icons/**/*.svg"/>
+ 				<include name="org/jedit/localization/*.props"/>
+ 			</fileset>
+ 		</jar>
+@@ -783,6 +784,7 @@
+ 				<include name="*.txt"/>
+ 				<include name="*.html"/>
+ 				<include name="*.png"/>
++				<include name="*.svg"/>
+ 				<include name="tips/**"/>
+ 			</fileset>
+ 		</copy>
+diff -ru jedit5.7.0/jEdit/ivy.xml jedit5.7.0-patched/jEdit/ivy.xml
+--- jedit5.7.0/jEdit/ivy.xml	2024-08-03 19:53:28.000000000 +0200
++++ jedit5.7.0-patched/jEdit/ivy.xml	2025-04-16 12:22:57.782535840 +0200
+@@ -94,5 +94,8 @@
+ 		<dependency org="com.google.code.findbugs" name="jsr305" rev="3.0.2"/>
+ 
+ 		<dependency org="com.evolvedbinary.appbundler" name="appbundler" rev="1.3.0" conf="appbundler"/>
++
++		<dependency org="com.formdev" name="flatlaf" rev="3.6"/>
++		<dependency org="com.formdev" name="flatlaf-extras" rev="3.6"/>
+ 	</dependencies>
+ </ivy-module>
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java	2025-04-16 21:35:23.519418287 +0200
+@@ -50,28 +50,28 @@
+ 		toolBar.add(Box.createGlue());
+ 
+ 		RolloverButton addMarker = new RolloverButton(
+-			GUIUtilities.loadIcon("Plus.png"));
++			GUIUtilities.loadIcon(jEdit.getProperty("add-marker.icon.small")));
+ 		addMarker.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
+ 			jEdit.getProperty("add-marker.label")));
+ 		addMarker.addActionListener(this);
+ 		addMarker.setActionCommand("add-marker");
+ 		toolBar.add(addMarker);
+ 
+-		previous = new RolloverButton(GUIUtilities.loadIcon("ArrowL.png"));
++		previous = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("prev-marker.icon.small")));
+ 		previous.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
+ 			jEdit.getProperty("prev-marker.label")));
+ 		previous.addActionListener(this);
+ 		previous.setActionCommand("prev-marker");
+ 		toolBar.add(previous);
+ 
+-		next = new RolloverButton(GUIUtilities.loadIcon("ArrowR.png"));
++		next = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("next-marker.icon.small")));
+ 		next.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
+ 			jEdit.getProperty("next-marker.label")));
+ 		next.addActionListener(this);
+ 		next.setActionCommand("next-marker");
+ 		toolBar.add(next);
+ 
+-		clear = new RolloverButton(GUIUtilities.loadIcon("Clear.png"));
++		clear = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("remove-all-markers.icon.small")));
+ 		clear.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
+ 			jEdit.getProperty("remove-all-markers.label")));
+ 		clear.addActionListener(this);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props	2024-08-03 19:53:20.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props	2025-04-17 00:11:31.583536114 +0200
+@@ -8,13 +8,15 @@
+ ###
+ 
+ #{{{ Common icons
+-common.add.icon=22x22/actions/list-add.png
+-common.remove.icon=22x22/actions/list-remove.png
+-common.moveUp.icon=22x22/actions/go-up.png
+-common.moveDown.icon=22x22/actions/go-down.png
+-common.clearAll.icon=22x22/actions/edit-clear.png
++common.add.icon=32x32/actions/list-add.svg?scale=0.7
++common.remove.icon=32x32/actions/list-remove.svg?scale=0.7
++common.moveUp.icon=32x32/actions/go-up.svg?scale=0.7
++common.moveDown.icon=32x32/actions/go-down.svg?scale=0.7
++common.clearAll.icon=32x32/actions/edit-clear.svg?scale=0.7
+ logo.icon.small=16x16/apps/jedit.png
+ logo.icon.medium=32x32/apps/jedit.png
++navigate-backwards.icon=idea-icons/expui/general/chevronLeft.svg?scale=1.2
++navigate-forwards.icon=idea-icons/expui/general/chevronRight.svg?scale=1.2
+ 
+ #}}}
+ 
+@@ -28,7 +30,7 @@
+ defer=false
+ startup=true
+ 
+-broken-image.icon=22x22/status/image-missing.png
++broken-image.icon=32x32/status/image-missing.svg?scale=0.7
+ dropdown-arrow.icon=ToolbarMenu.gif
+ #}}}
+ 
+@@ -39,68 +41,69 @@
+ 	buffer-options combined-options - \
+ 	plugin-manager - help
+ 
+-new-file.icon=22x22/actions/document-new.png
+-open-file.icon=22x22/actions/document-open.png
+-save.icon=22x22/actions/document-save.png
+-close-buffer.icon=22x22/actions/document-close.png
+-global-close-buffer.icon=22x22/actions/document-close.png
+-print.icon=22x22/actions/document-print.png
++new-file.icon=32x32/actions/document-new.svg?scale=0.7
++open-file.icon=32x32/actions/document-open.svg?scale=0.7
++save.icon=32x32/actions/document-save.svg?scale=0.7
++close-buffer.icon=32x32/actions/process-stop.svg?scale=0.7
++global-close-buffer.icon=32x32/actions/process-stop.svg?scale=0.7
++print.icon=32x32/actions/document-print.svg?scale=0.7
+ page-setup.icon=22x22/actions/printer-setup.png
+-undo.icon=22x22/actions/edit-undo.png
+-redo.icon=22x22/actions/edit-redo.png
+-cut.icon=22x22/actions/edit-cut.png
+-copy.icon=22x22/actions/edit-copy.png
+-paste.icon=22x22/actions/edit-paste.png
+-find.icon=22x22/actions/edit-find.png
+-find-next.icon=22x22/actions/edit-find-next.png
+-new-view.icon=22x22/actions/window-new.png
++undo.icon=32x32/actions/edit-undo.svg?scale=0.7
++redo.icon=32x32/actions/edit-redo.svg?scale=0.7
++cut.icon=32x32/actions/edit-cut.svg?scale=0.7
++copy.icon=32x32/actions/edit-copy.svg?scale=0.7
++paste.icon=32x32/actions/edit-paste.svg?scale=0.7
++find.icon=32x32/actions/edit-find.svg?scale=0.7
++find-prev.icon=32x32/actions/go-previous.svg?scale=0.7
++find-next.icon=32x32/actions/go-next.svg?scale=0.7
++new-view.icon=32x32/actions/window-new.svg?scale=0.7
+ unsplit.icon=22x22/actions/window-unsplit.png
+ split-horizontal.icon=22x22/actions/window-split-horizontal.png
+ split-vertical.icon=22x22/actions/window-split-vertical.png
+-buffer-options.icon=22x22/actions/document-properties.png
+-global-options.icon=22x22/categories/preferences-system.png
+-combined-options.icon=22x22/categories/preferences-system.png
++buffer-options.icon=32x32/actions/document-properties.svg?scale=0.7
++global-options.icon=32x32/categories/preferences-system.svg?scale=0.7
++combined-options.icon=32x32/categories/preferences-system.svg?scale=0.7
+ plugin-manager.icon=22x22/places/plugins.png
+-help.icon=22x22/apps/help-browser.png
++help.icon=22x22/apps/help-browser.svg
+ 
+ #{{{ Icon list for tool bar editor
+ icons=22x22/actions/resize-horisontal.png \
+-	22x22/actions/go-down.png \
+-	22x22/actions/go-previous.png \
+-	22x22/actions/go-next.png \
+-	22x22/actions/go-home.png \
+-	22x22/actions/go-up.png \
+-	22x22/actions/go-first.png \
+-	22x22/actions/go-last.png \
+-	22x22/actions/go-parent.png \
+-	22x22/actions/document-close.png \
+-	22x22/actions/edit-undo.png \
+-	22x22/actions/edit-redo.png \
+-	22x22/actions/edit-cut.png \
+-	22x22/actions/edit-paste.png \
+-	22x22/actions/edit-delete.png \
+-	22x22/actions/edit-clear.png \
+-	22x22/actions/edit-find-next.png \
+-	22x22/actions/edit-find-in-folder.png \
+-	22x22/actions/edit-find.png \
+-	22x22/actions/edit-copy.png \
++	22x22/actions/go-down.svg \
++	22x22/actions/go-previous.svg \
++	22x22/actions/go-next.svg \
++	32x32/actions/go-home.svg?scale=0.7 \
++	22x22/actions/go-up.svg \
++	22x22/actions/go-first.svg \
++	22x22/actions/go-last.svg \
++	22x22/actions/go-up.svg \
++	32x32/actions/process-stop.svg?scale=0.7 \
++	32x32/actions/edit-undo.svg?scale=0.7 \
++	32x32/actions/edit-redo.svg?scale=0.7 \
++	32x32/actions/edit-cut.svg?scale=0.7 \
++	32x32/actions/edit-paste.svg?scale=0.7 \
++	scalable/actions/edit-delete.svg \
++	22x22/actions/edit-clear.svg \
++	22x22/actions/go-next.svg \
++	32x32/actions/system-search.svg?scale=0.7 \
++	32x32/actions/edit-find.svg?scale=0.7 \
++	32x32/actions/edit-copy.svg?scale=0.7 \
+ 	22x22/actions/copy-to-buffer.png \
+-	22x22/actions/list-remove.png \
+-	22x22/actions/list-add.png \
+-	22x22/actions/folder-new.png \
+-	22x22/actions/window-new.png \
+-	22x22/actions/document-new.png \
+-	22x22/actions/document-open.png \
++	32x32/actions/list-remove.svg?scale=0.7 \
++	32x32/actions/list-add.svg?scale=0.7 \
++	32x32/actions/folder-new.svg?scale=0.7 \
++	32x32/actions/document-new.svg?scale=0.7 \
++	32x32/actions/document-new.svg?scale=0.7 \
++	32x32/actions/document-open.svg?scale=0.7 \
+ 	22x22/actions/document-reload2.png \
+-	22x22/actions/document-properties.png \
+-	22x22/actions/document-save.png \
+-	22x22/actions/document-save-all.png \
+-	22x22/actions/document-save-as.png \
++	32x32/actions/document-properties.svg?scale=0.7 \
++	32x32/actions/document-save.svg?scale=0.7 \
++	32x32/actions/document-save-all.svg?scale=0.5 \
++	32x32/actions/document-save-as.svg?scale=0.7 \
+ 	22x22/actions/printer-setup.png \
+-	22x22/actions/process-stop.png \
+-	22x22/actions/media-playback-pause.png \
+-	22x22/actions/media-playback-start.png \
+-	22x22/actions/view-refresh.png \
++	22x22/actions/system-log-out.svg \
++	22x22/actions/media-playback-pause.svg \
++	22x22/actions/media-playback-start.svg \
++	22x22/actions/view-refresh.svg \
+ 	22x22/actions/application-run.png \
+ 	22x22/actions/edit-find-multiple.png \
+ 	22x22/actions/edit-find-single.png \
+@@ -109,18 +112,18 @@
+ 	22x22/actions/window-unsplit.png \
+ 	22x22/actions/zoom-in.png \
+ 	22x22/actions/zoom-out.png \
+-	22x22/apps/utilities-terminal.png \
+-	22x22/apps/system-file-manager.png \
+-	22x22/apps/internet-web-browser.png \
+-	22x22/apps/help-browser.png \
+-	22x22/apps/system-installer.png \
+-	22x22/status/image-missing.png \
+-	22x22/status/folder-visiting.png \
+-	22x22/devices/drive-harddisk.png \
+-	22x22/devices/media-floppy.png \
+-	22x22/devices/printer.png \
++	22x22/apps/utilities-terminal.svg \
++	32x32/apps/system-file-manager.svg?scale=0.7 \
++	32x32/apps/internet-web-browser.svg?scale=0.7 \
++	22x22/apps/help-browser.svg \
++	32x32/apps/system-installer.svg?scale=0.7 \
++	32x32/status/image-missing.svg?scale=0.7 \
++	32x32/status/folder-visiting.svg?scale=0.7 \
++	32x32/devices/drive-harddisk.svg?scale=0.7 \
++	22x22/devices/media-floppy.svg \
++	32x32/devices/printer.svg?scale=0.7 \
+ 	22x22/places/plugins.png \
+-	22x22/categories/preferences-system.png \
++	32x32/categories/preferences-system.svg?scale=0.7 \
+ 	Blank24.gif
+ #}}}
+ 
+@@ -163,31 +166,31 @@
+ 	 print \
+ 	 - \
+ 	 exit
+-new-file.icon.small=16x16/actions/document-new.png
+-new-file-in-mode.icon.small=16x16/actions/document-new.png
+-open-file.icon.small=16x16/actions/document-open.png
+-reload.icon.small=16x16/actions/view-refresh.png
+-reload-all.icon.small=16x16/actions/view-refresh.png
+-close-buffer.icon.small=16x16/actions/document-close.png
+-closeall-bufferset.icon.small=16x16/actions/document-close.png
+-closeall-except-active.icon.small=16x16/actions/document-close.png
+-global-close-buffer.icon.small=16x16/actions/document-close.png
+-close-all.icon.small=16x16/actions/document-close.png
+-save.icon.small=16x16/actions/document-save.png
+-save-as.icon.small=16x16/actions/document-save-as.png
+-save-a-copy-as.icon.small=16x16/actions/document-save-as.png
+-save-all.icon.small=16x16/actions/document-save-all.png
+-print.icon.small=16x16/actions/document-print.png
+-page-setup.icon.small=16x16/actions/document-properties.png
+-exit.icon.small=16x16/actions/process-stop.png
+-exit.icon.medium=22x22/actions/process-stop.png
++new-file.icon.small=32x32/actions/document-new.svg?scale=0.5
++new-file-in-mode.icon.small=32x32/actions/document-new.svg?scale=0.5
++open-file.icon.small=32x32/actions/document-open.svg?scale=0.5
++reload.icon.small=16x16/actions/view-refresh.svg
++reload-all.icon.small=16x16/actions/view-refresh.svg
++close-buffer.icon.small=32x32/actions/process-stop.svg?scale=0.5
++closeall-bufferset.icon.small=32x32/actions/process-stop.svg?scale=0.5
++closeall-except-active.icon.small=32x32/actions/process-stop.svg?scale=0.5
++global-close-buffer.icon.small=32x32/actions/process-stop.svg?scale=0.5
++close-all.icon.small=32x32/actions/process-stop.svg?scale=0.5
++save.icon.small=32x32/actions/document-save.svg?scale=0.5
++save-as.icon.small=32x32/actions/document-save-as.svg?scale=0.5
++save-a-copy-as.icon.small=32x32/actions/document-save-as.svg?scale=0.5
++save-all.icon.small=32x32/actions/document-save.svg?scale=0.5
++print.icon.small=32x32/actions/document-print.svg?scale=0.5
++page-setup.icon.small=32x32/actions/document-properties.svg?scale=0.5
++exit.icon.small=16x16/actions/system-log-out.svg
++exit.icon.medium=22x22/actions/system-log-out.svg
+ 
+ #{{{ Recent Files menu
+ recent-files.code=new RecentFilesProvider();
+ #}}}
+ 
+ reload-encoding.code=new ReloadWithEncodingProvider();
+-reload-encoding.icon.small=16x16/actions/view-refresh.png
++reload-encoding.icon.small=16x16/actions/view-refresh.svg
+ #}}}
+ 
+ #{{{ Edit menu
+@@ -211,12 +214,12 @@
+ 	 %text \
+ 	 %indent \
+ 	 %source
+-undo.icon.small=16x16/actions/edit-undo.png
+-redo.icon.small=16x16/actions/edit-redo.png
+-cut.icon.small=16x16/actions/edit-cut.png
+-copy.icon.small=16x16/actions/edit-copy.png
+-paste.icon.small=16x16/actions/edit-paste.png
+-select-all.icon.small=16x16/actions/edit-select-all.png
++undo.icon.small=32x32/actions/edit-undo.svg?scale=0.5
++redo.icon.small=32x32/actions/edit-redo.svg?scale=0.5
++cut.icon.small=32x32/actions/edit-cut.svg?scale=0.5
++copy.icon.small=32x32/actions/edit-copy.svg?scale=0.5
++paste.icon.small=32x32/actions/edit-paste.svg?scale=0.5
++select-all.icon.small=16x16/actions/edit-select-all.svg
+ 
+ #{{{ More Clipboard menu
+ clipboard=cut-append \
+@@ -308,16 +311,18 @@
+ 	   regexp \
+ 	   - \
+ 	   hypersearch-results
+-find.icon.small=22x22/actions/edit-find.png
+-find-next.icon.small=22x22/actions/edit-find-next.png
+-search-in-directory.icon.small=22x22/actions/edit-find-in-folder.png
+-replace-in-selection.icon.small=22x22/actions/edit-find-replace.png
+-replace-and-find-next.icon.small=22x22/actions/edit-find-replace.png
+-replace-all.icon.small=22x22/actions/edit-find-replace.png
+-quick-search.icon.small=22x22/actions/edit-find.png
+-hypersearch.icon.small=22x22/actions/edit-find-multiple.png
+-quick-search-word.icon.small=22x22/actions/edit-find.png
+-hypersearch-word.icon.small=22x22/actions/edit-find.png
++find.icon.small=32x32/actions/edit-find.svg?scale=0.7
++find-prev.icon.small=32x32/actions/go-previous.svg?scale=0.7
++find-next.icon.small=32x32/actions/go-next.svg?scale=0.7
++search-in-open-buffers.icon.small=32x32/actions/system-search.svg?scale=0.7
++search-in-directory.icon.small=32x32/actions/system-search.svg?scale=0.7
++replace-in-selection.icon.small=32x32/actions/edit-find-replace.svg?scale=0.7
++replace-and-find-next.icon.small=32x32/actions/edit-find-replace.svg?scale=0.7
++replace-all.icon.small=32x32/actions/edit-find-replace.svg?scale=0.7
++quick-search.icon.small=32x32/actions/edit-find.svg?scale=0.7
++hypersearch.icon.small=32x32/actions/edit-find.svg?scale=0.7
++quick-search-word.icon.small=32x32/actions/edit-find.svg?scale=0.7
++hypersearch-word.icon.small=32x32/actions/edit-find.svg?scale=0.7
+ #}}}
+ 
+ #{{{ Markers menu
+@@ -336,12 +341,12 @@
+ 	  view-markers \
+ 	  -
+ markers.code=new MarkersProvider();
+-add-marker.icon.small=22x22/actions/bookmark-new.png
+-add-marker-shortcut.icon.small=22x22/actions/bookmark-new.png
+-remove-all-markers.icon.small=22x22/actions/edit-clear.png
+-goto-marker.icon.small=22x22/actions/go-jump.png
+-prev-marker.icon.small=22x22/actions/go-previous.png
+-next-marker.icon.small=22x22/actions/go-next.png
++add-marker.icon.small=32x32/actions/bookmark-new.svg?scale=0.7
++add-marker-shortcut.icon.small=32x32/actions/bookmark-new.svg?scale=0.7
++remove-all-markers.icon.small=32x32/actions/edit-clear.svg?scale=0.7
++goto-marker.icon.small=32x32/actions/go-jump.svg?scale=0.7
++prev-marker.icon.small=32x32/actions/go-previous.svg?scale=0.7
++next-marker.icon.small=32x32/actions/go-next.svg?scale=0.7
+ #}}}
+ 
+ #{{{ Folding menu
+@@ -388,9 +393,12 @@
+ 	 - \
+ 	 set-view-title \
+ 	 toggle-full-screen
+-new-view.icon.small=16x16/actions/window-new.png
+-new-plain-view.icon.small=16x16/actions/window-new.png
+-close-view.icon.small=16x16/actions/document-close.png
++new-view.icon.small=32x32/actions/window-new.svg?scale=0.5
++new-plain-view.icon.small=32x32/actions/window-new.svg?scale=0.5
++close-view.icon.small=32x32/actions/process-stop.svg?scale=0.5
++prev-buffer.icon.small=32x32/actions/go-previous.svg?scale=0.5
++next-buffer.icon.small=32x32/actions/go-next.svg?scale=0.5
++recent-buffer.icon.small=32x32/actions/go-up.svg?scale=0.5
+ 
+ #{{{ Scrolling menu
+ scrolling=scroll-to-current-line \
+@@ -454,9 +462,9 @@
+ 	  - \
+ 	  %quick-options
+ 
+-buffer-options.icon.small=16x16/actions/document-properties.png
+-global-options.icon.small=16x16/categories/preferences-system.png
+-combined-options.icon.small=16x16/categories/preferences-system.png
++buffer-options.icon.small=32x32/actions/document-properties.svg?scale=0.5
++global-options.icon.small=32x32/categories/preferences-system.svg?scale=0.5
++combined-options.icon.small=32x32/categories/preferences-system.svg?scale=0.5
+ 
+ #{{{ Recent Directories menu
+ recent-directories.code=new RecentDirectoriesProvider();
+@@ -518,9 +526,9 @@
+ 	   rescan-macros \
+ 	   -
+ macros.code=new MacrosProvider();
+-new-macro.icon.small=16x16/actions/document-new.png
+-record-macro.icon.small=16x16/actions/media-record.png
+-stop-recording.icon.small=16x16/actions/media-playback-stop.png
++new-macro.icon.small=32x32/actions/document-new.svg?scale=0.5
++record-macro.icon.small=16x16/actions/media-record.svg
++stop-recording.icon.small=32x32/actions/media-playback-stop.svg?scale=0.5
+ #}}}
+ 
+ #{{{ Plugins menu
+@@ -771,7 +779,7 @@
+ 
+ #{{{ HyperSearch results dialog
+ hypersearch-results.clear.icon=22x22/actions/edit-clear.png
+-hypersearch-results.stop.icon=22x22/actions/process-stop.png
++hypersearch-results.stop.icon=22x22/actions/system-log-out.png
+ hypersearch-results.multi.multiple.icon=22x22/actions/edit-find-multiple.png
+ hypersearch-results.multi.single.icon=22x22/actions/edit-find-single.png
+ hypersearch-results.match.highlight.icon=22x22/actions/edit-find-highlight-match.png
+@@ -784,8 +792,8 @@
+ #}}}
+ 
+ #{{{ Help Viewer
+-helpviewer.back.icon=22x22/actions/go-previous.png
+-helpviewer.forward.icon=22x22/actions/go-next.png
++helpviewer.back.icon=32x32/actions/go-previous.svg?scale=0.7
++helpviewer.forward.icon=32x32/actions/go-next.svg?scale=0.7
+ #}}}
+ 
+ #}}}
+@@ -809,9 +817,9 @@
+ 
+ #{{{ Abbreviations pane
+ options.abbrevs.code=new AbbrevsOptionPane();
+-options.abbrevs.add.icon=22x22/actions/list-add.png
+-options.abbrevs.edit.icon=22x22/actions/document-properties.png
+-options.abbrevs.remove.icon=22x22/actions/list-remove.png
++options.abbrevs.add.icon=32x32/actions/list-add.svg?scale=0.7
++options.abbrevs.edit.icon=32x32/actions/document-properties.svg?scale=0.7
++options.abbrevs.remove.icon=32x32/actions/list-remove.svg?scale=0.7
+ #}}}
+ 
+ #{{{ Appearance pane
+@@ -840,11 +848,11 @@
+ 
+ #{{{ Context Menu pane
+ options.context.code=new ContextOptionPane();
+-options.context.add.icon=22x22/actions/list-add.png
+-options.context.remove.icon=22x22/actions/list-remove.png
+-options.context.moveUp.icon=22x22/actions/go-up.png
+-options.context.moveDown.icon=22x22/actions/go-down.png
+-options.context.reset.icon=22x22/actions/edit-clear.png
++options.context.add.icon=32x32/actions/list-add.svg?scale=0.7
++options.context.remove.icon=32x32/actions/list-remove.svg?scale=0.7
++options.context.moveUp.icon=32x32/actions/go-up.svg?scale=0.7
++options.context.moveDown.icon=32x32/actions/go-down.svg?scale=0.7
++options.context.reset.icon=32x32/actions/edit-clear.svg?scale=0.7
+ options.context.includeOptionsLink=true
+ #}}}
+ 
+@@ -906,12 +914,12 @@
+ 
+ #{{{ Tool Bar pane
+ options.toolbar.code=new ToolBarOptionPane();
+-options.toolbar.add.icon=22x22/actions/list-add.png
+-options.toolbar.remove.icon=22x22/actions/list-remove.png
+-options.toolbar.moveUp.icon=22x22/actions/go-up.png
+-options.toolbar.moveDown.icon=22x22/actions/go-down.png
+-options.toolbar.reset.icon=22x22/actions/edit-clear.png
+-options.toolbar.edit.icon=22x22/actions/document-properties.png
++options.toolbar.add.icon=32x32/actions/list-add.svg?scale=0.7
++options.toolbar.remove.icon=32x32/actions/list-remove.svg?scale=0.7
++options.toolbar.moveUp.icon=22x22/actions/go-up.svg
++options.toolbar.moveDown.icon=22x22/actions/go-down.svg
++options.toolbar.reset.icon=22x22/actions/edit-clear.svg
++options.toolbar.edit.icon=32x32/actions/document-properties.svg?scale=0.7
+ #}}}
+ 
+ #{{{ View pane
+@@ -949,7 +957,8 @@
+ vfs.browser.default-filter=*[^~#]
+ vfs.browser.filter-enabled=true
+ vfs.browser.file.icon=16x16/mimetypes/text-x-generic.png
+-vfs.browser.icon.small=16x16/apps/system-file-manager.png
++vfs.browser.icon=32x32/apps/system-file-manager.svg?scale=0.7
++vfs.browser.icon.small=32x32/apps/system-file-manager.svg?scale=0.5
+ vfs.browser.open-file.icon=16x16/actions/edit-select-all.png
+ vfs.browser.dir.icon=16x16/places/folder.png
+ vfs.browser.open-dir.icon=16x16/status/folder-open.png
+@@ -1007,13 +1016,13 @@
+ plugin-manager.mirror-url=http://plugins.jedit.org/export/mirror_list.php
+ 
+ #{{{ Plugin management
+-manage-plugins.restore.icon=22x22/actions/document-open.png
+-manage-plugins.save.icon=22x22/actions/document-save.png
++manage-plugins.restore.icon=32x32/actions/document-open.svg?scale=0.7
++manage-plugins.save.icon=32x32/actions/document-save.svg?scale=0.7
+ #}}}
+ 
+ #{{{ Plugin installation
+-install-plugins.choose-plugin-set.icon=22x22/actions/document-open.png
+-install-plugins.clear-plugin-set.icon=22x22/actions/edit-clear.png
++install-plugins.choose-plugin-set.icon=32x32/actions/document-open.svg?scale=0.7
++install-plugins.clear-plugin-set.icon=22x22/actions/edit-clear.svg
+ #}}}
+ 
+ #}}}
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java	2025-04-16 16:12:29.542089148 +0200
+@@ -78,12 +78,12 @@
+ 		buttons.setBorder(new EmptyBorder(3,0,0,0));
+ 		buttons.setLayout(new BoxLayout(buttons,BoxLayout.X_AXIS));
+ 		ActionListener actionHandler = new ActionHandler();
+-		JButton add = new RolloverButton(GUIUtilities.loadIcon("Plus.png"));
++		JButton add = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.add.icon")));
+ 		add.setToolTipText(jEdit.getProperty("common.add"));
+ 		add.addActionListener(e -> colorsModel.add());
+ 		buttons.add(add);
+ 		buttons.add(Box.createHorizontalStrut(6));
+-		remove = new RolloverButton(GUIUtilities.loadIcon("Minus.png"));
++		remove = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.remove.icon")));
+ 		remove.setToolTipText(jEdit.getProperty("common.remove"));
+ 		remove.addActionListener(e ->
+ 		{
+@@ -93,12 +93,12 @@
+ 		});
+ 		buttons.add(remove);
+ 		buttons.add(Box.createHorizontalStrut(6));
+-		moveUp = new RolloverButton(GUIUtilities.loadIcon("ArrowU.png"));
++		moveUp = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveUp.icon")));
+ 		moveUp.setToolTipText(jEdit.getProperty("common.moveUp"));
+ 		moveUp.addActionListener(actionHandler);
+ 		buttons.add(moveUp);
+ 		buttons.add(Box.createHorizontalStrut(6));
+-		moveDown = new RolloverButton(GUIUtilities.loadIcon("ArrowD.png"));
++		moveDown = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveDown.icon")));
+ 		moveDown.setToolTipText(jEdit.getProperty("common.moveDown"));
+ 		moveDown.addActionListener(actionHandler);
+ 		buttons.add(moveDown);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java	2025-04-16 16:12:37.730958557 +0200
+@@ -160,12 +160,12 @@
+ 		buttons.setBorder(new EmptyBorder(3,0,0,0));
+ 		buttons.setLayout(new BoxLayout(buttons,BoxLayout.X_AXIS));
+ 		buttons.add(Box.createHorizontalStrut(6));
+-		moveUp = new RolloverButton(GUIUtilities.loadIcon("ArrowU.png"));
++		moveUp = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveUp.icon")));
+ 		moveUp.setToolTipText(jEdit.getProperty("options.status.moveUp"));
+ 		moveUp.addActionListener(e -> moveUp());
+ 		buttons.add(moveUp);
+ 		buttons.add(Box.createHorizontalStrut(6));
+-		moveDown = new RolloverButton(GUIUtilities.loadIcon("ArrowD.png"));
++		moveDown = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveDown.icon")));
+ 		moveDown.setToolTipText(jEdit.getProperty("options.status.moveDown"));
+ 		moveDown.addActionListener(e -> moveDown());
+ 		buttons.add(moveDown);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java	2025-04-16 21:45:44.861713409 +0200
+@@ -54,7 +54,7 @@
+ 		toolBar.add(Box.createGlue());
+ 
+ 		RolloverButton pasteRegister = new RolloverButton(
+-			GUIUtilities.loadIcon("Paste.png"));
++			GUIUtilities.loadIcon(jEdit.getProperty("paste.icon")));
+ 		pasteRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
+ 			jEdit.getProperty("paste-string-register.label")));
+ 		pasteRegister.addActionListener(e -> insertRegister());
+@@ -62,7 +62,7 @@
+ 		toolBar.add(pasteRegister);
+ 
+ 		RolloverButton clearRegister = new RolloverButton(
+-			GUIUtilities.loadIcon("Clear.png"));
++			GUIUtilities.loadIcon(jEdit.getProperty("common.clearAll.icon")));
+ 		clearRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
+ 			jEdit.getProperty("clear-string-register.label")));
+ 		clearRegister.addActionListener(e -> clearSelectedIndex());
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/menu_accelerator
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/menu_accelerator	Wed Apr 23 16:58:49 2025 +0200
@@ -0,0 +1,144 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2025-04-23 14:40:22.714447724 +0200
+@@ -99,7 +99,7 @@
+ 
+ 		if(shortcut != null)
+ 		{
+-			FontMetrics fm = getFontMetrics(EnhancedMenuItem.acceleratorFont);
++			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
+ 			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
+ 		}
+ 		return d;
+@@ -114,11 +114,9 @@
+ 		if(shortcut != null)
+ 		{
+ 			Graphics2D g2 = (Graphics2D)g;
+-			g.setFont(EnhancedMenuItem.acceleratorFont);
++			g.setFont(GUIUtilities.menuAcceleratorFont());
+ 			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+-			g.setColor(getModel().isArmed() ?
+-				EnhancedMenuItem.acceleratorSelectionForeground :
+-				EnhancedMenuItem.acceleratorForeground);
++			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
+ 			FontMetrics fm = g.getFontMetrics();
+ 			Insets insets = getInsets();
+ 			g.drawString(shortcut,getWidth() - (fm.stringWidth(
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2025-04-23 14:26:16.757848751 +0200
+@@ -94,7 +94,7 @@
+ 
+ 		if(shortcut != null)
+ 		{
+-			FontMetrics fm = getFontMetrics(acceleratorFont);
++			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
+ 			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
+ 		}
+ 		return d;
+@@ -109,11 +109,9 @@
+ 		if(shortcut != null)
+ 		{
+ 			Graphics2D g2 = (Graphics2D)g;
+-			g.setFont(acceleratorFont);
++			g.setFont(GUIUtilities.menuAcceleratorFont());
+ 			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+-			g.setColor(getModel().isArmed() ?
+-				acceleratorSelectionForeground :
+-				acceleratorForeground);
++			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
+ 			FontMetrics fm = g.getFontMetrics();
+ 			Insets insets = getInsets();
+ 			g.drawString(shortcut,getWidth() - (fm.stringWidth(
+@@ -122,12 +120,6 @@
+ 		}
+ 	} //}}}
+ 
+-	//{{{ Package-private members
+-	static Font acceleratorFont;
+-	static Color acceleratorForeground;
+-	static Color acceleratorSelectionForeground;
+-	//}}}
+-
+ 	//{{{ Private members
+ 
+ 	//{{{ Instance variables
+@@ -135,25 +127,5 @@
+ 	private String shortcut;
+ 	//}}}
+ 
+-	//{{{ Class initializer
+-	static
+-	{
+-		acceleratorFont = GUIUtilities.menuAcceleratorFont();
+-
+-		acceleratorForeground = UIManager
+-			.getColor("MenuItem.acceleratorForeground");
+-		if(acceleratorForeground == null)
+-		{
+-			acceleratorForeground = Color.black;
+-		}
+-
+-		acceleratorSelectionForeground = UIManager
+-			.getColor("MenuItem.acceleratorSelectionForeground");
+-		if(acceleratorSelectionForeground == null)
+-		{
+-			acceleratorSelectionForeground = Color.black;
+-		}
+-	} //}}}
+-
+ 	//}}}
+ }
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2025-04-23 14:27:48.829375470 +0200
+@@ -107,7 +107,7 @@
+ 
+ 			if(shortcut != null)
+ 			{
+-				FontMetrics fm = getFontMetrics(acceleratorFont);
++				FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
+ 				d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
+ 			}
+ 			return d;
+@@ -124,11 +124,9 @@
+ 			if(shortcut != null)
+ 			{
+ 				Graphics2D g2 = (Graphics2D)g;
+-				g.setFont(acceleratorFont);
++				g.setFont(GUIUtilities.menuAcceleratorFont());
+ 				g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+-				g.setColor(getModel().isArmed() ?
+-					acceleratorSelectionForeground :
+-					acceleratorForeground);
++				g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
+ 				FontMetrics fm = g.getFontMetrics();
+ 				Insets insets = getInsets();
+ 				g.drawString(shortcut,getWidth() - (fm.stringWidth(
+@@ -140,9 +138,6 @@
+ 		//{{{ Private members
+ 		private final String shortcutProp;
+ 		private final char shortcut;
+-		private static final Font acceleratorFont;
+-		private static final Color acceleratorForeground;
+-		private static final Color acceleratorSelectionForeground;
+ 
+ 		//{{{ getShortcut() method
+ 		private String getShortcut()
+@@ -162,16 +157,6 @@
+ 			}
+ 		} //}}}
+ 
+-		//{{{ Class initializer
+-		static
+-		{
+-			acceleratorFont = GUIUtilities.menuAcceleratorFont();
+-			acceleratorForeground = UIManager
+-				.getColor("MenuItem.acceleratorForeground");
+-			acceleratorSelectionForeground = UIManager
+-				.getColor("MenuItem.acceleratorSelectionForeground");
+-		} //}}}
+-
+ 		//}}}
+ 	} //}}}
+ }
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/menus_and_sidekick
--- a/src/Tools/jEdit/patches/menus_and_sidekick	Wed Apr 23 14:42:38 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-10-29 11:50:54.062016616 +0100
-@@ -1094,9 +1094,7 @@
- 				return new Font("Monospaced", Font.PLAIN, 12);
- 			}
- 			else {
--				Font font2 =
--					new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
--						Font.PLAIN, font1.getSize());
-+				Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
- 				FontRenderContext frc = new FontRenderContext(null, true, false);
- 				float scale =
- 					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-08-03 19:53:16.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-11-15 20:22:26.451538237 +0100
-@@ -225,8 +225,11 @@
- 			else
- 				this.message.setText(" ");
- 		}
--		else
--			this.message.setText(message);
-+		else {
-+			Exception exn = new Exception();
-+			if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
-+				this.message.setText(message);
-+		}
- 	} //}}}
- 
- 	//{{{ setMessageComponent() method
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-11-15 18:42:41.560326356 +0100
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-11-15 20:33:52.458587638 +0100
-@@ -1617,6 +1617,21 @@
- 	}
- 	//}}}
- 
-+	//{{{ isPopupTrigger() method
-+	/**
-+	 * Returns if the specified event is the popup trigger event.
-+	 * This implements precisely defined behavior, as opposed to
-+	 * MouseEvent.isPopupTrigger().
-+	 * @param evt The event
-+	 * @since jEdit 3.2pre8
-+	 * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
-+	 */
-+	@Deprecated
-+	public static boolean isPopupTrigger(MouseEvent evt)
-+	{
-+		return GenericGUIUtilities.isPopupTrigger(evt);
-+	} //}}}
-+
- 	//{{{ init() method
- 	static void init()
- 	{
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/props
--- a/src/Tools/jEdit/patches/props	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/patches/props	Wed Apr 23 16:58:49 2025 +0200
@@ -1,6 +1,15 @@
 diff -ru jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props
 --- jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props	2024-08-03 19:53:22.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props	2024-10-29 11:50:54.066016546 +0100
++++ jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props	2025-04-22 22:08:19.298392180 +0200
+@@ -70,7 +70,7 @@
+ #}}}
+ 
+ #{{{ Tool bar
+-view.search.find=Search for:
++view.search.find=Search:
+ view.search.close-tooltip=Hide search bar (ESCAPE)
+ 
+ view.action.prompt=Action:
 @@ -1282,8 +1282,7 @@
  	The most likely reason is that the JAR file is corrupt; try\n\
  	reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
@@ -11,3 +20,12 @@
  plugin-error.already-loaded=Two copies installed. Please remove one of the \
  	two copies.
  plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
+@@ -1610,7 +1609,7 @@
+ options.gutter.optionalComponents=Optional gutter components
+ options.gutter.lineNumbers=Line numbers
+ options.gutter.minLineNumberDigits=Minimal number of digits to reserve for line numbers:
+-options.gutter.selectionAreaEnabled=Line selection area when line numbers are not shown
++options.gutter.selectionAreaEnabled=Line selection area (with icons) when line numbers are not shown
+ options.gutter.selectionAreaBgColor=Selection area background color:
+ options.gutter.selectionAreaWidth=Selection area width (in pixels):
+ options.gutter.font=Gutter font:
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/patches/status_bar
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/status_bar	Wed Apr 23 16:58:49 2025 +0200
@@ -0,0 +1,17 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-11-15 20:22:26.451538237 +0100
+@@ -225,8 +225,11 @@
+ 			else
+ 				this.message.setText(" ");
+ 		}
+-		else
+-			this.message.setText(message);
++		else {
++			Exception exn = new Exception();
++			if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
++				this.message.setText(message);
++		}
+ 	} //}}}
+ 
+ 	//{{{ setMessageComponent() method
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -403,7 +403,7 @@
     text_field =>
 
     // see https://forums.oracle.com/thread/1361677
-    if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
+    if (GUI.is_macos_laf()) text_field.setCaret(new DefaultCaret)
 
     // owned by GUI thread
     private var completion_popup: Option[Completion_Popup] = None
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -12,11 +12,13 @@
 
 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
 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 {
@@ -140,9 +142,19 @@
         GUI_Thread.assert {}
 
         val gutter = text_area.getGutter
-        val sel_width = GutterOptionPane.getSelectionAreaWidth
-        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
-        val FOLD_MARKER_SIZE = 12
+        val gutter_width = gutter.getWidth
+        val gutter_insets = gutter.getBorder.getBorderInsets(gutter)
+
+        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
+
+        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
 
         val buffer = model.buffer
         JEdit_Lib.buffer_lock(buffer) {
@@ -155,19 +167,27 @@
               rendering.gutter_content(line_range) match {
                 case Some((icon, color)) =>
                   // icons within selection area
-                  if (!gutter.isExpanded &&
-                      gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12) {
-                    val x0 =
-                      (FOLD_MARKER_SIZE + sel_width - border_width - icon.getIconWidth) max 10
-                    val y0 =
-                      y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
-                    icon.paintIcon(gutter, gfx, x0, y0)
+                  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)
+
+                    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
+                  // background only
                   else {
                     val y0 = y + i * line_height
                     gfx.setColor(color)
-                    gfx.fillRect(0, y0, gutter.getWidth, line_height)
+                    gfx.fillRect(0, y0, gutter_width, line_height)
                   }
                 case None =>
               }
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Apr 23 16:58:49 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
@@ -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,23 +386,8 @@
 
   /* icons */
 
-  def load_icon(name: String): Icon = {
-    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
-  }
-
-  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 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 23 16:58:49 2025 +0200
@@ -266,7 +266,7 @@
 
   /* search */
 
-  private val search_label: Component = new Label(jEdit.getProperty("search.find")) {
+  private val search_label: Component = new Label(jEdit.getProperty("view.search.find")) {
     tooltip = "Search and highlight output via regular expression"
   }
 
diff -r 32a6228f543d -r 9390f8e3b1c1 src/Tools/jEdit/src/process_indicator.scala
--- a/src/Tools/jEdit/src/process_indicator.scala	Wed Apr 23 14:42:38 2025 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala	Wed Apr 23 16:58:49 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