--- a/Admin/components/components.sha1 Wed May 21 20:13:43 2025 +0200
+++ b/Admin/components/components.sha1 Wed May 21 21:51:56 2025 +0200
@@ -278,6 +278,7 @@
5637fb7b2d0c24ca4d1ffe18156d2f6a8ec9fab3 jedit-20250515.tar.gz
62cce488b1c5541de7a56a4a49537037da2bfd44 jedit-20250516.tar.gz
5789aa61bb37a8003a2b6e1037d217057e51cdc9 jedit-20250520.tar.gz
+a141f565676050b8b6e6e97629778f96a81d9706 jedit-20250521.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Wed May 21 20:13:43 2025 +0200
+++ b/Admin/components/main Wed May 21 21:51:56 2025 +0200
@@ -15,7 +15,7 @@
isabelle_setup-20240327
javamail-20250122
jdk-21.0.6
-jedit-20250520
+jedit-20250521
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.18.3
--- a/src/Pure/Admin/component_jedit.scala Wed May 21 20:13:43 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala Wed May 21 21:51:56 2025 +0200
@@ -474,10 +474,12 @@
view.gutter.selectionAreaBgColor.dark=\#ff282828
view.gutter.structureHighlightColor.dark=\#ffcccccc
view.lineHighlightColor.dark=\#ff1d0a0a
+view.multipleSelectionColor.dark=\#ff006622
view.selectionColor.dark=\#ff0f4982
view.status.background.dark=\#ff333333
view.status.foreground.dark=\#ffffffff
-view.status.memory.background.dark=\#ff66699a
+view.status.highlight.dark=\#ff141414
+view.status.memory.background.dark=\#ff666699
view.status.memory.foreground.dark=\#ffcccccc
view.structureHighlightColor.dark=\#ffffff00
view.style.comment1.dark=color\:\#ff87ceeb
--- a/src/Tools/jEdit/patches/docking Wed May 21 20:13:43 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2025-05-20 15:21:47.892811800 +0200
-@@ -45,14 +45,15 @@
- * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
- * @since jEdit 4.0pre1
- */
--public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
--{
-+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
- private String dockableName;
-
- //{{{ FloatingWindowContainer constructor
- public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
- boolean clone)
- {
-+ super(dockableWindowManager.getView());
-+
- this.dockableWindowManager = dockableWindowManager;
-
- dockableWindowManager.addPropertyChangeListener(this);
-@@ -62,7 +63,7 @@
-
- Box caption = new Box(BoxLayout.X_AXIS);
- caption.add(menu = new RolloverButton(GUIUtilities
-- .loadIcon(jEdit.getProperty("dropdown-arrow.icon"))));
-+ .loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon"))));
- menu.addMouseListener(new MouseHandler());
- menu.setToolTipText(jEdit.getProperty("docking.menu.label"));
- Box separatorBox = new Box(BoxLayout.Y_AXIS);
-@@ -87,7 +88,6 @@
- pack();
- Container parent = dockableWindowManager.getView();
- GUIUtilities.loadGeometry(this, parent, dockableName);
-- GUIUtilities.addSizeSaver(this, parent, dockableName);
- KeyListener listener = dockableWindowManager.closeListener(dockableName);
- addKeyListener(listener);
- getContentPane().addKeyListener(listener);
-@@ -154,8 +154,11 @@
- @Override
- public void dispose()
- {
-- entry.container = null;
-- entry.win = null;
-+ GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
-+ if (entry != null) {
-+ entry.container = null;
-+ entry.win = null;
-+ }
- super.dispose();
- } //}}}
-
--- a/src/Tools/jEdit/patches/gui Wed May 21 20:13:43 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1136 +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 2025-05-20 15:40:14.181962645 +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,48 @@
-
- //{{{ Colors and styles
-
-+ public static Color menuAcceleratorForeground(boolean selection) {
-+ Color color =
-+ UIManager.getColor(selection ?
-+ "MenuItem.acceleratorSelectionForeground" :
-+ "MenuItem.acceleratorForeground");
-+
-+ if (color == null) color = defaultFgColor();
-+
-+ return color;
-+ }
-+
-+ public static boolean isDarkLaf()
-+ {
-+ return com.formdev.flatlaf.FlatLaf.isLafDark();
-+ }
-+
-+ public static Color defaultBgColor()
-+ {
-+ return isDarkLaf() ? Color.BLACK : Color.WHITE;
-+ }
-+
-+ public static Color defaultFgColor()
-+ {
-+ return isDarkLaf() ? Color.WHITE : Color.BLACK;
-+ }
-+
-+ public static String getTheme()
-+ {
-+ return isDarkLaf() ? "dark" : "";
-+ }
-+
-+ public static String getThemeSuffix()
-+ {
-+ return getThemeSuffix(".");
-+ }
-+
-+ public static String getThemeSuffix(String s)
-+ {
-+ String t = getTheme();
-+ return t.isEmpty() ? t : s + t;
-+ }
-+
- //{{{ getStyleString() method
- /**
- * Converts a style into it's string representation.
-@@ -1407,8 +1466,8 @@
- {
- for (Component child: win.getComponents())
- {
-- child.setBackground(jEdit.getColorProperty("view.bgColor", Color.WHITE));
-- child.setForeground(jEdit.getColorProperty("view.fgColor", Color.BLACK));
-+ child.setBackground(jEdit.getColorProperty("view.bgColor", defaultBgColor()));
-+ child.setForeground(jEdit.getColorProperty("view.fgColor"));
- if (child instanceof JTextPane)
- ((JTextPane)child).setUI(new javax.swing.plaf.basic.BasicEditorPaneUI());
- if (child instanceof Container)
-@@ -1596,7 +1655,7 @@
- deprecatedIcons.put("NextFile.png", "22x22/go-last.png");
- deprecatedIcons.put("PreviousFile.png","22x22/go-first.png");
-
-- deprecatedIcons.put("closebox.gif", "10x10/actions/close.png");
-+ deprecatedIcons.put("closebox.gif", "32x32/actions/process-stop.svg?scale=0.33");
- deprecatedIcons.put("normal.gif", "10x10/status/document-unmodified.png");
- deprecatedIcons.put("readonly.gif", "10x10/emblem/emblem-readonly.png");
- deprecatedIcons.put("dirty.gif", "10x10/status/document-modified.png");
-@@ -1619,6 +1678,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 -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-05-20 13:46:50.541586193 +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,8 +30,8 @@
- defer=false
- startup=true
-
--broken-image.icon=22x22/status/image-missing.png
--dropdown-arrow.icon=ToolbarMenu.gif
-+broken-image.icon=32x32/status/image-missing.svg?scale=0.7
-+dropdown-arrow.icon=idea-icons/general/buttonDropTriangle.svg
- #}}}
-
- #{{{ Tool bar
-@@ -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-05-14 10:51:38.322378673 +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);
-@@ -209,8 +209,7 @@
- {
- entries.add(new Entry(glob,
- jEdit.getColorProperty(
-- "vfs.browser.colors." + i + ".color",
-- Color.black)));
-+ "vfs.browser.colors." + i + ".color")));
- i++;
- }
- } //}}}
-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 -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2025-05-15 21:20:18.075698848 +0200
-@@ -674,6 +674,12 @@
- return value;
- } //}}}
-
-+ public static String getThemeProperty(String name)
-+ {
-+ String s = GUIUtilities.getThemeSuffix();
-+ return s.isEmpty() ? getProperty(name) : getProperty(name + s, getProperty(name));
-+ }
-+
- //{{{ getProperty() method
- /**
- * Returns the property with the specified name.<p>
-@@ -859,7 +865,7 @@
- */
- public static Color getColorProperty(String name)
- {
-- return getColorProperty(name,Color.black);
-+ return getColorProperty(name, GUIUtilities.defaultFgColor());
- }
-
- /**
-@@ -870,7 +876,7 @@
- */
- public static Color getColorProperty(String name, Color def)
- {
-- String value = getProperty(name);
-+ String value = getThemeProperty(name);
- if(value == null)
- return def;
- else
-@@ -886,7 +892,7 @@
- */
- public static void setColorProperty(String name, Color value)
- {
-- setProperty(name, SyntaxUtilities.getColorHexString(value));
-+ setThemeProperty(name, SyntaxUtilities.getColorHexString(value));
- } //}}}
-
- //{{{ getColorMatrixProperty() method
-@@ -936,6 +942,11 @@
- public static void setProperty(String name, String value)
- {
- propMgr.setProperty(name,value);
-+ }
-+
-+ public static void setThemeProperty(String name, String value)
-+ {
-+ setProperty(name + GUIUtilities.getThemeSuffix(), value);
- } //}}}
-
- //{{{ setTemporaryProperty() method
-@@ -4233,7 +4244,7 @@
- } //}}}
-
- //{{{ gotoMarker() method
-- private static void gotoMarker(final View view, final Buffer buffer,
-+ public static void gotoMarker(final View view, final Buffer buffer,
- final String marker)
- {
- AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2024-08-03 19:53:16.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2025-05-13 16:29:14.196283445 +0200
-@@ -58,7 +58,7 @@
- public static final DataFlavor BufferDataFlavor = new DataFlavor(BufferTransferableData.class, DataFlavor.javaJVMLocalObjectMimeType);
-
- // actual colors will be set in constructor, here are just fallback values
-- static Color defaultColor = Color.BLACK;
-+ static Color defaultColor = GUIUtilities.defaultFgColor();
- static Color defaultBGColor = Color.LIGHT_GRAY;
-
- public BufferSwitcher(final EditPane editPane)
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2024-08-03 19:53:16.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2025-05-14 11:05:39.544481221 +0200
-@@ -413,7 +413,7 @@
- {
- this.list = list;
- debugColor = jEdit.getColorProperty("log-viewer.message.debug.color", Color.BLUE);
-- messageColor = jEdit.getColorProperty("log-viewer.message.message.color", Color.BLACK);
-+ messageColor = jEdit.getColorProperty("log-viewer.message.message.color");
- noticeColor = jEdit.getColorProperty("log-viewer.message.notice.color", Color.GREEN);
- warningColor = jEdit.getColorProperty("log-viewer.message.warning.color", Color.ORANGE);
- errorColor = jEdit.getColorProperty("log-viewer.message.error.color", Color.RED);
-diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java
---- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2024-08-03 19:53:14.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2025-05-14 10:51:16.530755624 +0200
-@@ -1302,8 +1302,7 @@
- colors.add(new ColorEntry(
- Pattern.compile(StandardUtilities.globToRE(glob)),
- jEdit.getColorProperty(
-- "vfs.browser.colors." + i + ".color",
-- Color.black)));
-+ "vfs.browser.colors." + i + ".color")));
- }
- catch(PatternSyntaxException e)
- {
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
---- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2025-05-14 15:20:40.515623017 +0200
-@@ -35,6 +35,7 @@
- import org.gjt.sp.jedit.syntax.SyntaxStyle;
- import org.gjt.sp.jedit.syntax.Token;
- import org.gjt.sp.jedit.IPropertyManager;
-+import org.gjt.sp.jedit.GUIUtilities;
-
- import static java.util.stream.Collectors.joining;
- //}}}
-@@ -49,6 +50,15 @@
- public class SyntaxUtilities
- {
- public static IPropertyManager propertyManager;
-+
-+ public static String getThemeProperty(String name)
-+ {
-+ String s = GUIUtilities.getThemeSuffix();
-+ String a = propertyManager.getProperty(name);
-+ String b = propertyManager.getProperty(name + s);
-+ return b == null ? a : b;
-+ }
-+
- private static final Pattern COLOR_MATRIX_PATTERN = Pattern.compile("(?x)\n" +
- "^\n" +
- "\\s*+ # optionally preceded by whitespace\n" +
-@@ -125,7 +135,7 @@
- */
- public static Color parseColor(String name)
- {
-- return parseColor(name, Color.black);
-+ return parseColor(name, GUIUtilities.defaultFgColor());
- } //}}}
-
- //{{{ parseColor() method
-@@ -267,7 +277,7 @@
- if(s.startsWith("color:"))
- {
- if(color)
-- fgColor = parseColor(s.substring(6), Color.black);
-+ fgColor = parseColor(s.substring(6), GUIUtilities.defaultFgColor());
- }
- else if(s.startsWith("bgColor:"))
- {
-@@ -311,7 +321,7 @@
- boolean color)
- throws IllegalArgumentException
- {
-- return parseStyle(str, family, size, color, Color.black);
-+ return parseStyle(str, family, size, color, GUIUtilities.defaultFgColor());
- } //}}}
-
- //{{{ loadStyles() methods
-@@ -347,9 +357,7 @@
- String styleName = "view.style."
- + Token.tokenToString((byte)i)
- .toLowerCase(Locale.ENGLISH);
-- styles[i] = parseStyle(
-- propertyManager.getProperty(styleName),
-- family,size,color);
-+ styles[i] = parseStyle(getThemeProperty(styleName),family,size,color);
- }
- catch(Exception e)
- {
-@@ -357,8 +365,28 @@
- }
- }
-
-- return styles;
-+ styles[0] =
-+ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", GUIUtilities.defaultFgColor()),
-+ null, new Font(family, 0, size));
-+ return _styleExtender.extendStyles(styles);
- } //}}}
-
-+ /**
-+ * Extended styles derived from the user-specified style array.
-+ */
-+
-+ public static class StyleExtender
-+ {
-+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
-+ {
-+ return styles;
-+ }
-+ }
-+ volatile private static StyleExtender _styleExtender = new StyleExtender();
-+ public static void setStyleExtender(StyleExtender ext)
-+ {
-+ _styleExtender = ext;
-+ }
-+
- private SyntaxUtilities(){}
- }
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-05-14 15:46:36.934878462 +0200
-@@ -43,6 +43,7 @@
- import org.gjt.sp.jedit.msg.BufferChanging;
- import org.gjt.sp.jedit.msg.BufferUpdate;
- import org.gjt.sp.jedit.msg.EditPaneUpdate;
-+import org.gjt.sp.jedit.msg.PositionChanging;
- import org.gjt.sp.jedit.msg.PropertiesChanged;
- import org.gjt.sp.jedit.options.GeneralOptionPane;
- import org.gjt.sp.jedit.options.GutterOptionPane;
-@@ -380,9 +381,11 @@
- buffer.unsetProperty(Buffer.CARET_POSITIONED);
-
-
-- if(caret != -1)
-+ if(caret != -1) {
- textArea.setCaretPosition(Math.min(caret,
- buffer.getLength()));
-+ EditBus.send(new PositionChanging(this));
-+ }
-
- // set any selections
- Selection[] selection = caretInfo.selection;
-@@ -1029,7 +1032,7 @@
- for(int i = 0; i <= 3; i++)
- {
- foldLineStyle[i] = SyntaxUtilities.parseStyle(
-- jEdit.getProperty("view.style.foldLine." + i),
-+ jEdit.getThemeProperty("view.style.foldLine." + i),
- defaultFont,defaultFontSize, true);
- }
- painter.setFoldLineStyle(foldLineStyle);
-diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java
---- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2025-05-14 15:46:44.805742407 +0200
-@@ -95,7 +95,7 @@
- Font font = getFont();
- String family = font.getFamily();
- int size = font.getSize();
-- invalidStyle = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), family, size, true);
-+ invalidStyle = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), family, size, true);
- defaultForeground = getForeground();
- defaultBackground = getBackground();
- }
-diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java
---- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2024-08-03 19:53:16.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2025-05-14 15:46:52.413610804 +0200
-@@ -102,7 +102,7 @@
- String defaultFont = jEdit.getProperty("view.font");
- int defaultFontSize = jEdit.getIntegerProperty("view.fontsize", 12);
- SyntaxStyle invalid = SyntaxUtilities.parseStyle(
-- jEdit.getProperty("view.style.invalid"),
-+ jEdit.getThemeProperty("view.style.invalid"),
- defaultFont,defaultFontSize, true);
- foregroundColor = invalid.getForegroundColor();
- setForeground(foregroundColor);
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2025-05-15 21:23:50.047418219 +0200
-@@ -222,8 +222,7 @@
- {
- for (StyleChoice ch : styleChoices)
- {
-- jEdit.setProperty(ch.property,
-- GUIUtilities.getStyleString(ch.style));
-+ jEdit.setThemeProperty(ch.property,GUIUtilities.getStyleString(ch.style));
- }
- } //}}}
-
-@@ -233,7 +232,7 @@
- Font font = new JLabel().getFont();
- styleChoices.add(new StyleChoice(label,
- property,
-- SyntaxUtilities.parseStyle(jEdit.getProperty(property),
-+ SyntaxUtilities.parseStyle(jEdit.getThemeProperty(property),
- font.getFamily(), font.getSize(), true)));
- } //}}}
-
-@@ -289,8 +288,8 @@
- else
- {
- // this part sucks
-- setBackground(jEdit.getColorProperty(
-- "view.bgColor"));
-+ setBackground(
-+ jEdit.getColorProperty("view.bgColor", GUIUtilities.defaultBgColor()));
- }
- setFont(style.getFont());
- }
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2025-05-14 15:48:00.821423396 +0200
-@@ -90,12 +90,12 @@
- String property = "view.style." + typeName.toLowerCase();
- Font font = new JLabel().getFont();
- SyntaxStyle currentStyle = SyntaxUtilities.parseStyle(
-- jEdit.getProperty(property), font.getFamily(), font.getSize(), true);
-+ jEdit.getThemeProperty(property), font.getFamily(), font.getSize(), true);
- SyntaxStyle style = new StyleEditor(textArea.getView(),
- currentStyle, typeName).getStyle();
- if(style != null)
- {
-- jEdit.setProperty(property, GUIUtilities.getStyleString(style));
-+ jEdit.setProperty(property + GUIUtilities.getThemeSuffix(), GUIUtilities.getStyleString(style));
- jEdit.propertiesChanged();
- }
- } //}}}
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-05-14 15:49:19.228054251 +0200
-@@ -51,6 +51,10 @@
- setFloatable(false);
- add(Box.createHorizontalStrut(2));
-
-+ if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) {
-+ add(GUIUtilities.loadToolBar("navigate-toolbar"));
-+ }
-+
- JLabel label = new JLabel(jEdit.getProperty("view.search.find"));
- add(label);
-
-@@ -59,7 +63,7 @@
- add(find = new HistoryTextField("find"));
- find.setSelectAllOnFocus(true);
-
-- SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), "Dialog", 12, true);
-+ SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), "Dialog", 12, true);
- errorBackground = style.getBackgroundColor();
- errorForeground = style.getForegroundColor();
- defaultBackground = find.getBackground();
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2024-08-03 19:53:20.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2025-05-20 15:21:59.692613480 +0200
-@@ -61,7 +61,7 @@
- ? "helpviewer.back.label"
- : "helpviewer.forward.label"));
- Box box = new Box(BoxLayout.X_AXIS);
-- drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
-+ drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
- drop_button.addActionListener(new DropActionHandler());
- box.add(arrow_button);
- box.add(drop_button);
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java 2025-05-20 16:27:48.111088672 +0200
-@@ -191,6 +191,7 @@
-
- if(optionPane != null)
- {
-+ deferredOptionPanes.clear();
- deferredOptionPanes.put(
- node,optionPane);
- }
-diff -ru jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java
---- jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java 2024-08-03 19:53:23.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java 2025-05-20 16:34:10.010928214 +0200
-@@ -151,6 +151,7 @@
-
- if (optionPane != null)
- {
-+ deferredOptionPanes.clear();
- deferredOptionPanes.put(node, optionPane);
- }
- else
--- a/src/Tools/jEdit/patches/laf_fonts Wed May 21 20:13:43 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-10-29 11:50:54.062016616 +0100
-@@ -414,7 +414,9 @@
-
- // adjust swing properties for button, menu, and label, and list and
- // textfield fonts
-- setFonts();
-+ if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
-+ setFonts();
-+ }
-
- // This is handled a little differently from other jEdit settings
- // as this flag needs to be known very early in the
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/main Wed May 21 21:51:56 2025 +0200
@@ -0,0 +1,1328 @@
+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-05-20 15:40:14.181962645 +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,48 @@
+
+ //{{{ Colors and styles
+
++ public static Color menuAcceleratorForeground(boolean selection) {
++ Color color =
++ UIManager.getColor(selection ?
++ "MenuItem.acceleratorSelectionForeground" :
++ "MenuItem.acceleratorForeground");
++
++ if (color == null) color = defaultFgColor();
++
++ return color;
++ }
++
++ public static boolean isDarkLaf()
++ {
++ return com.formdev.flatlaf.FlatLaf.isLafDark();
++ }
++
++ public static Color defaultBgColor()
++ {
++ return isDarkLaf() ? Color.BLACK : Color.WHITE;
++ }
++
++ public static Color defaultFgColor()
++ {
++ return isDarkLaf() ? Color.WHITE : Color.BLACK;
++ }
++
++ public static String getTheme()
++ {
++ return isDarkLaf() ? "dark" : "";
++ }
++
++ public static String getThemeSuffix()
++ {
++ return getThemeSuffix(".");
++ }
++
++ public static String getThemeSuffix(String s)
++ {
++ String t = getTheme();
++ return t.isEmpty() ? t : s + t;
++ }
++
+ //{{{ getStyleString() method
+ /**
+ * Converts a style into it's string representation.
+@@ -1407,8 +1466,8 @@
+ {
+ for (Component child: win.getComponents())
+ {
+- child.setBackground(jEdit.getColorProperty("view.bgColor", Color.WHITE));
+- child.setForeground(jEdit.getColorProperty("view.fgColor", Color.BLACK));
++ child.setBackground(jEdit.getColorProperty("view.bgColor", defaultBgColor()));
++ child.setForeground(jEdit.getColorProperty("view.fgColor"));
+ if (child instanceof JTextPane)
+ ((JTextPane)child).setUI(new javax.swing.plaf.basic.BasicEditorPaneUI());
+ if (child instanceof Container)
+@@ -1596,7 +1655,7 @@
+ deprecatedIcons.put("NextFile.png", "22x22/go-last.png");
+ deprecatedIcons.put("PreviousFile.png","22x22/go-first.png");
+
+- deprecatedIcons.put("closebox.gif", "10x10/actions/close.png");
++ deprecatedIcons.put("closebox.gif", "32x32/actions/process-stop.svg?scale=0.33");
+ deprecatedIcons.put("normal.gif", "10x10/status/document-unmodified.png");
+ deprecatedIcons.put("readonly.gif", "10x10/emblem/emblem-readonly.png");
+ deprecatedIcons.put("dirty.gif", "10x10/status/document-modified.png");
+@@ -1619,6 +1678,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 -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-05-20 13:46:50.541586193 +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,8 +30,8 @@
+ defer=false
+ startup=true
+
+-broken-image.icon=22x22/status/image-missing.png
+-dropdown-arrow.icon=ToolbarMenu.gif
++broken-image.icon=32x32/status/image-missing.svg?scale=0.7
++dropdown-arrow.icon=idea-icons/general/buttonDropTriangle.svg
+ #}}}
+
+ #{{{ Tool bar
+@@ -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-05-14 10:51:38.322378673 +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);
+@@ -209,8 +209,7 @@
+ {
+ entries.add(new Entry(glob,
+ jEdit.getColorProperty(
+- "vfs.browser.colors." + i + ".color",
+- Color.black)));
++ "vfs.browser.colors." + i + ".color")));
+ i++;
+ }
+ } //}}}
+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 -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2025-05-15 21:20:18.075698848 +0200
+@@ -674,6 +674,12 @@
+ return value;
+ } //}}}
+
++ public static String getThemeProperty(String name)
++ {
++ String s = GUIUtilities.getThemeSuffix();
++ return s.isEmpty() ? getProperty(name) : getProperty(name + s, getProperty(name));
++ }
++
+ //{{{ getProperty() method
+ /**
+ * Returns the property with the specified name.<p>
+@@ -859,7 +865,7 @@
+ */
+ public static Color getColorProperty(String name)
+ {
+- return getColorProperty(name,Color.black);
++ return getColorProperty(name, GUIUtilities.defaultFgColor());
+ }
+
+ /**
+@@ -870,7 +876,7 @@
+ */
+ public static Color getColorProperty(String name, Color def)
+ {
+- String value = getProperty(name);
++ String value = getThemeProperty(name);
+ if(value == null)
+ return def;
+ else
+@@ -886,7 +892,7 @@
+ */
+ public static void setColorProperty(String name, Color value)
+ {
+- setProperty(name, SyntaxUtilities.getColorHexString(value));
++ setThemeProperty(name, SyntaxUtilities.getColorHexString(value));
+ } //}}}
+
+ //{{{ getColorMatrixProperty() method
+@@ -936,6 +942,11 @@
+ public static void setProperty(String name, String value)
+ {
+ propMgr.setProperty(name,value);
++ }
++
++ public static void setThemeProperty(String name, String value)
++ {
++ setProperty(name + GUIUtilities.getThemeSuffix(), value);
+ } //}}}
+
+ //{{{ setTemporaryProperty() method
+@@ -4233,7 +4244,7 @@
+ } //}}}
+
+ //{{{ gotoMarker() method
+- private static void gotoMarker(final View view, final Buffer buffer,
++ public static void gotoMarker(final View view, final Buffer buffer,
+ final String marker)
+ {
+ AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2025-05-13 16:29:14.196283445 +0200
+@@ -58,7 +58,7 @@
+ public static final DataFlavor BufferDataFlavor = new DataFlavor(BufferTransferableData.class, DataFlavor.javaJVMLocalObjectMimeType);
+
+ // actual colors will be set in constructor, here are just fallback values
+- static Color defaultColor = Color.BLACK;
++ static Color defaultColor = GUIUtilities.defaultFgColor();
+ static Color defaultBGColor = Color.LIGHT_GRAY;
+
+ public BufferSwitcher(final EditPane editPane)
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2025-05-14 11:05:39.544481221 +0200
+@@ -413,7 +413,7 @@
+ {
+ this.list = list;
+ debugColor = jEdit.getColorProperty("log-viewer.message.debug.color", Color.BLUE);
+- messageColor = jEdit.getColorProperty("log-viewer.message.message.color", Color.BLACK);
++ messageColor = jEdit.getColorProperty("log-viewer.message.message.color");
+ noticeColor = jEdit.getColorProperty("log-viewer.message.notice.color", Color.GREEN);
+ warningColor = jEdit.getColorProperty("log-viewer.message.warning.color", Color.ORANGE);
+ errorColor = jEdit.getColorProperty("log-viewer.message.error.color", Color.RED);
+diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java
+--- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2025-05-14 10:51:16.530755624 +0200
+@@ -1302,8 +1302,7 @@
+ colors.add(new ColorEntry(
+ Pattern.compile(StandardUtilities.globToRE(glob)),
+ jEdit.getColorProperty(
+- "vfs.browser.colors." + i + ".color",
+- Color.black)));
++ "vfs.browser.colors." + i + ".color")));
+ }
+ catch(PatternSyntaxException e)
+ {
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2025-05-14 15:20:40.515623017 +0200
+@@ -35,6 +35,7 @@
+ import org.gjt.sp.jedit.syntax.SyntaxStyle;
+ import org.gjt.sp.jedit.syntax.Token;
+ import org.gjt.sp.jedit.IPropertyManager;
++import org.gjt.sp.jedit.GUIUtilities;
+
+ import static java.util.stream.Collectors.joining;
+ //}}}
+@@ -49,6 +50,15 @@
+ public class SyntaxUtilities
+ {
+ public static IPropertyManager propertyManager;
++
++ public static String getThemeProperty(String name)
++ {
++ String s = GUIUtilities.getThemeSuffix();
++ String a = propertyManager.getProperty(name);
++ String b = propertyManager.getProperty(name + s);
++ return b == null ? a : b;
++ }
++
+ private static final Pattern COLOR_MATRIX_PATTERN = Pattern.compile("(?x)\n" +
+ "^\n" +
+ "\\s*+ # optionally preceded by whitespace\n" +
+@@ -125,7 +135,7 @@
+ */
+ public static Color parseColor(String name)
+ {
+- return parseColor(name, Color.black);
++ return parseColor(name, GUIUtilities.defaultFgColor());
+ } //}}}
+
+ //{{{ parseColor() method
+@@ -267,7 +277,7 @@
+ if(s.startsWith("color:"))
+ {
+ if(color)
+- fgColor = parseColor(s.substring(6), Color.black);
++ fgColor = parseColor(s.substring(6), GUIUtilities.defaultFgColor());
+ }
+ else if(s.startsWith("bgColor:"))
+ {
+@@ -311,7 +321,7 @@
+ boolean color)
+ throws IllegalArgumentException
+ {
+- return parseStyle(str, family, size, color, Color.black);
++ return parseStyle(str, family, size, color, GUIUtilities.defaultFgColor());
+ } //}}}
+
+ //{{{ loadStyles() methods
+@@ -347,9 +357,7 @@
+ String styleName = "view.style."
+ + Token.tokenToString((byte)i)
+ .toLowerCase(Locale.ENGLISH);
+- styles[i] = parseStyle(
+- propertyManager.getProperty(styleName),
+- family,size,color);
++ styles[i] = parseStyle(getThemeProperty(styleName),family,size,color);
+ }
+ catch(Exception e)
+ {
+@@ -357,8 +365,28 @@
+ }
+ }
+
+- return styles;
++ styles[0] =
++ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", GUIUtilities.defaultFgColor()),
++ null, new Font(family, 0, size));
++ return _styleExtender.extendStyles(styles);
+ } //}}}
+
++ /**
++ * Extended styles derived from the user-specified style array.
++ */
++
++ public static class StyleExtender
++ {
++ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
++ {
++ return styles;
++ }
++ }
++ volatile private static StyleExtender _styleExtender = new StyleExtender();
++ public static void setStyleExtender(StyleExtender ext)
++ {
++ _styleExtender = ext;
++ }
++
+ private SyntaxUtilities(){}
+ }
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-05-14 15:46:36.934878462 +0200
+@@ -43,6 +43,7 @@
+ import org.gjt.sp.jedit.msg.BufferChanging;
+ import org.gjt.sp.jedit.msg.BufferUpdate;
+ import org.gjt.sp.jedit.msg.EditPaneUpdate;
++import org.gjt.sp.jedit.msg.PositionChanging;
+ import org.gjt.sp.jedit.msg.PropertiesChanged;
+ import org.gjt.sp.jedit.options.GeneralOptionPane;
+ import org.gjt.sp.jedit.options.GutterOptionPane;
+@@ -380,9 +381,11 @@
+ buffer.unsetProperty(Buffer.CARET_POSITIONED);
+
+
+- if(caret != -1)
++ if(caret != -1) {
+ textArea.setCaretPosition(Math.min(caret,
+ buffer.getLength()));
++ EditBus.send(new PositionChanging(this));
++ }
+
+ // set any selections
+ Selection[] selection = caretInfo.selection;
+@@ -1029,7 +1032,7 @@
+ for(int i = 0; i <= 3; i++)
+ {
+ foldLineStyle[i] = SyntaxUtilities.parseStyle(
+- jEdit.getProperty("view.style.foldLine." + i),
++ jEdit.getThemeProperty("view.style.foldLine." + i),
+ defaultFont,defaultFontSize, true);
+ }
+ painter.setFoldLineStyle(foldLineStyle);
+diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java
+--- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2025-05-14 15:46:44.805742407 +0200
+@@ -95,7 +95,7 @@
+ Font font = getFont();
+ String family = font.getFamily();
+ int size = font.getSize();
+- invalidStyle = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), family, size, true);
++ invalidStyle = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), family, size, true);
+ defaultForeground = getForeground();
+ defaultBackground = getBackground();
+ }
+diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java
+--- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2025-05-14 15:46:52.413610804 +0200
+@@ -102,7 +102,7 @@
+ String defaultFont = jEdit.getProperty("view.font");
+ int defaultFontSize = jEdit.getIntegerProperty("view.fontsize", 12);
+ SyntaxStyle invalid = SyntaxUtilities.parseStyle(
+- jEdit.getProperty("view.style.invalid"),
++ jEdit.getThemeProperty("view.style.invalid"),
+ defaultFont,defaultFontSize, true);
+ foregroundColor = invalid.getForegroundColor();
+ setForeground(foregroundColor);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2025-05-15 21:23:50.047418219 +0200
+@@ -222,8 +222,7 @@
+ {
+ for (StyleChoice ch : styleChoices)
+ {
+- jEdit.setProperty(ch.property,
+- GUIUtilities.getStyleString(ch.style));
++ jEdit.setThemeProperty(ch.property,GUIUtilities.getStyleString(ch.style));
+ }
+ } //}}}
+
+@@ -233,7 +232,7 @@
+ Font font = new JLabel().getFont();
+ styleChoices.add(new StyleChoice(label,
+ property,
+- SyntaxUtilities.parseStyle(jEdit.getProperty(property),
++ SyntaxUtilities.parseStyle(jEdit.getThemeProperty(property),
+ font.getFamily(), font.getSize(), true)));
+ } //}}}
+
+@@ -289,8 +288,8 @@
+ else
+ {
+ // this part sucks
+- setBackground(jEdit.getColorProperty(
+- "view.bgColor"));
++ setBackground(
++ jEdit.getColorProperty("view.bgColor", GUIUtilities.defaultBgColor()));
+ }
+ setFont(style.getFont());
+ }
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2025-05-14 15:48:00.821423396 +0200
+@@ -90,12 +90,12 @@
+ String property = "view.style." + typeName.toLowerCase();
+ Font font = new JLabel().getFont();
+ SyntaxStyle currentStyle = SyntaxUtilities.parseStyle(
+- jEdit.getProperty(property), font.getFamily(), font.getSize(), true);
++ jEdit.getThemeProperty(property), font.getFamily(), font.getSize(), true);
+ SyntaxStyle style = new StyleEditor(textArea.getView(),
+ currentStyle, typeName).getStyle();
+ if(style != null)
+ {
+- jEdit.setProperty(property, GUIUtilities.getStyleString(style));
++ jEdit.setProperty(property + GUIUtilities.getThemeSuffix(), GUIUtilities.getStyleString(style));
+ jEdit.propertiesChanged();
+ }
+ } //}}}
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-05-14 15:49:19.228054251 +0200
+@@ -51,6 +51,10 @@
+ setFloatable(false);
+ add(Box.createHorizontalStrut(2));
+
++ if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) {
++ add(GUIUtilities.loadToolBar("navigate-toolbar"));
++ }
++
+ JLabel label = new JLabel(jEdit.getProperty("view.search.find"));
+ add(label);
+
+@@ -59,7 +63,7 @@
+ add(find = new HistoryTextField("find"));
+ find.setSelectAllOnFocus(true);
+
+- SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), "Dialog", 12, true);
++ SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), "Dialog", 12, true);
+ errorBackground = style.getBackgroundColor();
+ errorForeground = style.getForegroundColor();
+ defaultBackground = find.getBackground();
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2024-08-03 19:53:20.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2025-05-20 15:21:59.692613480 +0200
+@@ -61,7 +61,7 @@
+ ? "helpviewer.back.label"
+ : "helpviewer.forward.label"));
+ Box box = new Box(BoxLayout.X_AXIS);
+- drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
++ drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
+ drop_button.addActionListener(new DropActionHandler());
+ box.add(arrow_button);
+ box.add(drop_button);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java 2025-05-20 16:27:48.111088672 +0200
+@@ -191,6 +191,7 @@
+
+ if(optionPane != null)
+ {
++ deferredOptionPanes.clear();
+ deferredOptionPanes.put(
+ node,optionPane);
+ }
+diff -ru jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java
+--- jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java 2024-08-03 19:53:23.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java 2025-05-20 16:34:10.010928214 +0200
+@@ -151,6 +151,7 @@
+
+ if (optionPane != null)
+ {
++ deferredOptionPanes.clear();
+ deferredOptionPanes.put(node, optionPane);
+ }
+ else
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2025-05-20 15:21:47.892811800 +0200
+@@ -45,14 +45,15 @@
+ * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
+ * @since jEdit 4.0pre1
+ */
+-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
+-{
++public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
+ private String dockableName;
+
+ //{{{ FloatingWindowContainer constructor
+ public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
+ boolean clone)
+ {
++ super(dockableWindowManager.getView());
++
+ this.dockableWindowManager = dockableWindowManager;
+
+ dockableWindowManager.addPropertyChangeListener(this);
+@@ -62,7 +63,7 @@
+
+ Box caption = new Box(BoxLayout.X_AXIS);
+ caption.add(menu = new RolloverButton(GUIUtilities
+- .loadIcon(jEdit.getProperty("dropdown-arrow.icon"))));
++ .loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon"))));
+ menu.addMouseListener(new MouseHandler());
+ menu.setToolTipText(jEdit.getProperty("docking.menu.label"));
+ Box separatorBox = new Box(BoxLayout.Y_AXIS);
+@@ -87,7 +88,6 @@
+ pack();
+ Container parent = dockableWindowManager.getView();
+ GUIUtilities.loadGeometry(this, parent, dockableName);
+- GUIUtilities.addSizeSaver(this, parent, dockableName);
+ KeyListener listener = dockableWindowManager.closeListener(dockableName);
+ addKeyListener(listener);
+ getContentPane().addKeyListener(listener);
+@@ -154,8 +154,11 @@
+ @Override
+ public void dispose()
+ {
+- entry.container = null;
+- entry.win = null;
++ GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
++ if (entry != null) {
++ entry.container = null;
++ entry.win = null;
++ }
+ super.dispose();
+ } //}}}
+
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2025-05-20 15:21:53.380719554 +0200
+@@ -53,6 +53,7 @@
+ import javax.swing.JComponent;
+ import javax.swing.JPanel;
+ import javax.swing.JPopupMenu;
++import javax.swing.JMenuItem;
+ import javax.swing.JToggleButton;
+ import javax.swing.UIManager;
+ import javax.swing.border.Border;
+@@ -99,7 +100,7 @@
+
+ closeBox.addActionListener(e -> show((DockableWindowManagerImpl.Entry)null));
+
+- menuBtn = new JButton(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
++ menuBtn = new JButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
+ menuBtn.setRequestFocusEnabled(false);
+ menuBtn.setToolTipText(jEdit.getProperty("view.docking.menu-tooltip"));
+ if(OperatingSystem.isMacOSLF())
+@@ -164,6 +165,7 @@
+ {
+ button = new JToggleButton();
+ button.setMargin(new Insets(1,1,1,1));
++ button.setFont(new JMenuItem().getFont());
+ }
+ GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
+ button.setRequestFocusEnabled(false);
+@@ -683,8 +685,6 @@
+ renderHints = new RenderingHints(
+ RenderingHints.KEY_ANTIALIASING,
+ RenderingHints.VALUE_ANTIALIAS_ON);
+- renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
+- RenderingHints.VALUE_FRACTIONALMETRICS_ON);
+ renderHints.put(RenderingHints.KEY_RENDERING,
+ RenderingHints.VALUE_RENDER_QUALITY);
+ } //}}}
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2025-05-20 15:21:39.685949775 +0200
+@@ -1195,6 +1195,7 @@
+ VFSFile[] selectedFiles = browserView.getSelectedFiles();
+
+ Buffer buffer = null;
++ String bufferMarker = null;
+
+ check_selected:
+ for (VFSFile file : selectedFiles)
+@@ -1244,7 +1245,10 @@
+ }
+
+ if (_buffer != null)
++ {
+ buffer = _buffer;
++ bufferMarker = file.getPathMarker();
++ }
+ }
+ // otherwise if a file is selected in OPEN_DIALOG or
+ // SAVE_DIALOG mode, just let the listener(s)
+@@ -1253,21 +1257,30 @@
+
+ if(buffer != null)
+ {
++ View gotoView = null;
++
+ switch(mode)
+ {
+ case M_OPEN:
+ view.setBuffer(buffer);
++ gotoView = view;
+ break;
+ case M_OPEN_NEW_VIEW:
+- jEdit.newView(view,buffer,false);
++ gotoView = jEdit.newView(view,buffer,false);
+ break;
+ case M_OPEN_NEW_PLAIN_VIEW:
+- jEdit.newView(view,buffer,true);
++ gotoView = jEdit.newView(view,buffer,true);
+ break;
+ case M_OPEN_NEW_SPLIT:
+ view.splitHorizontally().setBuffer(buffer);
++ gotoView = view;
+ break;
+ }
++
++ if (gotoView != null && bufferMarker != null)
++ {
++ jEdit.gotoMarker(gotoView, buffer, bufferMarker);
++ }
+ }
+
+ Object[] listeners = listenerList.getListenerList();
+@@ -1751,7 +1764,7 @@
+ //{{{ MenuButton constructor
+ MenuButton()
+ {
+- setIcon(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
++ setIcon(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
+ setHorizontalTextPosition(SwingConstants.LEADING);
+
+ // setRequestFocusEnabled(false);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-10-29 11:50:54.062016616 +0100
+@@ -302,6 +302,12 @@
+ }
+ } //}}}
+
++ //{{{ getPathMarker() method (for jEdit.gotoMarker)
++ public String getPathMarker()
++ {
++ return null;
++ } //}}}
++
+ //{{{ getPath() method
+ public String getPath()
+ {
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2025-05-21 15:34:14.464265550 +0200
+@@ -93,7 +93,7 @@
+ /* Icon Theme */
+ String[] themes = IconTheme.builtInNames();
+ iconThemes = new JComboBox<String>(themes);
+- addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes);
++ //addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes);
+ String oldTheme = IconTheme.get();
+ for (int i=0; i<themes.length; ++i)
+ {
+@@ -414,7 +414,9 @@
+
+ // adjust swing properties for button, menu, and label, and list and
+ // textfield fonts
+- setFonts();
++ if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
++ setFonts();
++ }
+
+ // This is handled a little differently from other jEdit settings
+ // as this flag needs to be known very early in the
--- a/src/Tools/jEdit/patches/panel_font Wed May 21 20:13:43 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-08-03 19:53:16.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2025-05-20 15:21:53.380719554 +0200
-@@ -53,6 +53,7 @@
- import javax.swing.JComponent;
- import javax.swing.JPanel;
- import javax.swing.JPopupMenu;
-+import javax.swing.JMenuItem;
- import javax.swing.JToggleButton;
- import javax.swing.UIManager;
- import javax.swing.border.Border;
-@@ -99,7 +100,7 @@
-
- closeBox.addActionListener(e -> show((DockableWindowManagerImpl.Entry)null));
-
-- menuBtn = new JButton(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
-+ menuBtn = new JButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
- menuBtn.setRequestFocusEnabled(false);
- menuBtn.setToolTipText(jEdit.getProperty("view.docking.menu-tooltip"));
- if(OperatingSystem.isMacOSLF())
-@@ -164,6 +165,7 @@
- {
- button = new JToggleButton();
- button.setMargin(new Insets(1,1,1,1));
-+ button.setFont(new JMenuItem().getFont());
- }
- GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
- button.setRequestFocusEnabled(false);
-@@ -683,8 +685,6 @@
- renderHints = new RenderingHints(
- RenderingHints.KEY_ANTIALIASING,
- RenderingHints.VALUE_ANTIALIAS_ON);
-- renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
-- RenderingHints.VALUE_FRACTIONALMETRICS_ON);
- renderHints.put(RenderingHints.KEY_RENDERING,
- RenderingHints.VALUE_RENDER_QUALITY);
- } //}}}
--- a/src/Tools/jEdit/patches/vfs_marker Wed May 21 20:13:43 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2025-05-20 15:21:39.685949775 +0200
-@@ -1195,6 +1195,7 @@
- VFSFile[] selectedFiles = browserView.getSelectedFiles();
-
- Buffer buffer = null;
-+ String bufferMarker = null;
-
- check_selected:
- for (VFSFile file : selectedFiles)
-@@ -1244,7 +1245,10 @@
- }
-
- if (_buffer != null)
-+ {
- buffer = _buffer;
-+ bufferMarker = file.getPathMarker();
-+ }
- }
- // otherwise if a file is selected in OPEN_DIALOG or
- // SAVE_DIALOG mode, just let the listener(s)
-@@ -1253,21 +1257,30 @@
-
- if(buffer != null)
- {
-+ View gotoView = null;
-+
- switch(mode)
- {
- case M_OPEN:
- view.setBuffer(buffer);
-+ gotoView = view;
- break;
- case M_OPEN_NEW_VIEW:
-- jEdit.newView(view,buffer,false);
-+ gotoView = jEdit.newView(view,buffer,false);
- break;
- case M_OPEN_NEW_PLAIN_VIEW:
-- jEdit.newView(view,buffer,true);
-+ gotoView = jEdit.newView(view,buffer,true);
- break;
- case M_OPEN_NEW_SPLIT:
- view.splitHorizontally().setBuffer(buffer);
-+ gotoView = view;
- break;
- }
-+
-+ if (gotoView != null && bufferMarker != null)
-+ {
-+ jEdit.gotoMarker(gotoView, buffer, bufferMarker);
-+ }
- }
-
- Object[] listeners = listenerList.getListenerList();
-@@ -1751,7 +1764,7 @@
- //{{{ MenuButton constructor
- MenuButton()
- {
-- setIcon(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
-+ setIcon(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
- setHorizontalTextPosition(SwingConstants.LEADING);
-
- // setRequestFocusEnabled(false);
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-08-03 19:53:14.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-10-29 11:50:54.062016616 +0100
-@@ -302,6 +302,12 @@
- }
- } //}}}
-
-+ //{{{ getPathMarker() method (for jEdit.gotoMarker)
-+ public String getPathMarker()
-+ {
-+ return null;
-+ } //}}}
-+
- //{{{ getPath() method
- public String getPath()
- {