# HG changeset patch
# User wenzelm
# Date 1747838043 -7200
# Node ID 1db11efcd355aef40833cf4f901939c489a18e3f
# Parent  b5b3082c986607d78d44bbd5f1b6cd7f807a3ff3
suppress other icon themes: always use default "tango" (which includes "idea-icons") -- requires to update jedit component;

diff -r b5b3082c9866 -r 1db11efcd355 src/Tools/jEdit/patches/laf_fonts
--- a/src/Tools/jEdit/patches/laf_fonts	Wed May 21 15:13:31 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +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 -r b5b3082c9866 -r 1db11efcd355 src/Tools/jEdit/patches/main
--- a/src/Tools/jEdit/patches/main	Wed May 21 15:13:31 2025 +0200
+++ b/src/Tools/jEdit/patches/main	Wed May 21 16:34:03 2025 +0200
@@ -1303,3 +1303,26 @@
  	//{{{ getPath() method
  	public String getPath()
  	{
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2025-05-21 15:34:14.464265550 +0200
+@@ -93,7 +93,7 @@
+ 		/* Icon Theme */
+ 		String[] themes = IconTheme.builtInNames();
+ 		iconThemes = new JComboBox<String>(themes);
+-		addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes);
++		//addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes);
+ 		String oldTheme = IconTheme.get();
+ 		for (int i=0; i<themes.length; ++i)
+ 		{
+@@ -414,7 +414,9 @@
+ 
+ 		// adjust swing properties for button, menu, and label, and list and
+ 		// textfield fonts
+-		setFonts();
++		if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
++			setFonts();
++		}
+ 
+ 		// This is handled a little differently from other jEdit settings
+ 		// as this flag needs to be known very early in the