# HG changeset patch
# User wenzelm
# Date 1747747944 -7200
# Node ID 9f85679fd8998c20bba02f7e8145f9f86bd92e62
# Parent  38f5ecbb457496b15059c26f22b57f46f3db438d
proper scalable icon, also for dark mode -- requires to update jedit component;

diff -r 38f5ecbb4574 -r 9f85679fd899 src/Tools/jEdit/patches/docking
--- 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();
diff -r 38f5ecbb4574 -r 9f85679fd899 src/Tools/jEdit/patches/gui
--- 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);
diff -r 38f5ecbb4574 -r 9f85679fd899 src/Tools/jEdit/patches/panel_font
--- 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();	
diff -r 38f5ecbb4574 -r 9f85679fd899 src/Tools/jEdit/patches/vfs_marker
--- 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