--- a/src/Tools/jEdit/patches/docking Tue May 20 15:18:35 2025 +0200
+++ b/src/Tools/jEdit/patches/docking Tue May 20 15:32:24 2025 +0200
@@ -1,6 +1,6 @@
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 2024-10-29 11:50:54.062016616 +0100
++++ 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
@@ -19,6 +19,15 @@
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();
--- a/src/Tools/jEdit/patches/gui Tue May 20 15:18:35 2025 +0200
+++ b/src/Tools/jEdit/patches/gui Tue May 20 15:32:24 2025 +0200
@@ -241,7 +241,7 @@
clear.addActionListener(this);
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props 2024-08-03 19:53:20.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-04-17 00:11:31.583536114 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-05-20 13:46:50.541586193 +0200
@@ -8,13 +8,15 @@
###
@@ -263,15 +263,17 @@
#}}}
-@@ -28,7 +30,7 @@
+@@ -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=ToolbarMenu.gif
++dropdown-arrow.icon=idea-icons/general/buttonDropTriangle.svg
#}}}
+ #{{{ Tool bar
@@ -39,68 +41,69 @@
buffer-options combined-options - \
plugin-manager - help
@@ -1089,3 +1091,15 @@
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);
--- a/src/Tools/jEdit/patches/panel_font Tue May 20 15:18:35 2025 +0200
+++ b/src/Tools/jEdit/patches/panel_font Tue May 20 15:32:24 2025 +0200
@@ -1,6 +1,6 @@
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 2024-10-29 11:50:54.062016616 +0100
++++ 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;
@@ -9,6 +9,15 @@
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();
--- a/src/Tools/jEdit/patches/vfs_marker Tue May 20 15:18:35 2025 +0200
+++ b/src/Tools/jEdit/patches/vfs_marker Tue May 20 15:32:24 2025 +0200
@@ -1,6 +1,6 @@
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 2024-10-29 11:50:54.058016686 +0100
++++ 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();
@@ -53,6 +53,15 @@
}
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