# HG changeset patch # User wenzelm # Date 1747857833 -7200 # Node ID 629fa9278081ed7c166017f26a4e0bafe3d7f1a4 # Parent 565545b7fe9d20a683fde5bcff1d82d09ab71506# Parent 565aa4b28070feec3d7eb5d16d3fcc92ad0e68a7 merged diff -r 565545b7fe9d -r 629fa9278081 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed May 21 21:48:42 2025 +0200 +++ b/Admin/components/components.sha1 Wed May 21 22:03:53 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 diff -r 565545b7fe9d -r 629fa9278081 Admin/components/main --- a/Admin/components/main Wed May 21 21:48:42 2025 +0200 +++ b/Admin/components/main Wed May 21 22:03:53 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 diff -r 565545b7fe9d -r 629fa9278081 src/Pure/Admin/component_jedit.scala --- a/src/Pure/Admin/component_jedit.scala Wed May 21 21:48:42 2025 +0200 +++ b/src/Pure/Admin/component_jedit.scala Wed May 21 22:03:53 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 diff -r 565545b7fe9d -r 629fa9278081 src/Tools/jEdit/patches/docking --- a/src/Tools/jEdit/patches/docking Wed May 21 21:48:42 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(); - } //}}} - diff -r 565545b7fe9d -r 629fa9278081 src/Tools/jEdit/patches/gui --- a/src/Tools/jEdit/patches/gui Wed May 21 21:48:42 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 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 @@ - - - -+ - - - -@@ -783,6 +784,7 @@ - - - -+ - - - -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 @@ - - - -+ -+ -+ - - -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.

-@@ -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 -r 565545b7fe9d -r 629fa9278081 src/Tools/jEdit/patches/laf_fonts --- a/src/Tools/jEdit/patches/laf_fonts Wed May 21 21:48:42 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 diff -r 565545b7fe9d -r 629fa9278081 src/Tools/jEdit/patches/main --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/main Wed May 21 22:03:53 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 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 @@ + + + ++ + + + +@@ -783,6 +784,7 @@ + + + ++ + + + +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 @@ + + + ++ ++ ++ + + +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.

+@@ -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(themes); +- addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes); ++ //addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes); + String oldTheme = IconTheme.get(); + for (int i=0; i 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 -r 565545b7fe9d -r 629fa9278081 src/Tools/jEdit/patches/vfs_marker --- a/src/Tools/jEdit/patches/vfs_marker Wed May 21 21:48:42 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() - {