# HG changeset patch
# User wenzelm
# Date 1745412846 -7200
# Node ID b47b65bd707f9495c27ca0a9900313c6a81761f7
# Parent  782519a6ebb48645258a5d91e202168c3c076c41
proper painting of menu accelerator in dark mode;

diff -r 782519a6ebb4 -r b47b65bd707f Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Apr 23 13:32:16 2025 +0200
+++ b/Admin/components/components.sha1	Wed Apr 23 14:54:06 2025 +0200
@@ -273,6 +273,7 @@
 cab6dca89dc2e0d922e92cc47df07941a3c6b29c jedit-20250415.tar.gz
 23297ab36a853247a17f87b94a29654f3259b341 jedit-20250417.tar.gz
 a291746959e64916e8504b89dca804186d4eb8a1 jedit-20250422.tar.gz
+07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r 782519a6ebb4 -r b47b65bd707f Admin/components/main
--- a/Admin/components/main	Wed Apr 23 13:32:16 2025 +0200
+++ b/Admin/components/main	Wed Apr 23 14:54:06 2025 +0200
@@ -15,7 +15,7 @@
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250422
+jedit-20250423
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3
diff -r 782519a6ebb4 -r b47b65bd707f src/Tools/jEdit/patches/gui_utilities
--- a/src/Tools/jEdit/patches/gui_utilities	Wed Apr 23 13:32:16 2025 +0200
+++ b/src/Tools/jEdit/patches/gui_utilities	Wed Apr 23 14:54:06 2025 +0200
@@ -1,6 +1,6 @@
 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-04-22 22:11:53.770185212 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2025-04-23 14:28:53.149349418 +0200
 @@ -42,6 +42,8 @@
  import java.net.URL;
  import java.util.*;
@@ -90,10 +90,21 @@
  				FontRenderContext frc = new FontRenderContext(null, true, false);
  				float scale =
  					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
-@@ -1107,6 +1124,11 @@
+@@ -1107,6 +1124,22 @@
  
  	//{{{ Colors and styles
  
++	public static Color menuAcceleratorForeground(boolean selection) {
++		Color color =
++			UIManager.getColor(selection ?
++				"MenuItem.acceleratorSelectionForeground" :
++				"MenuItem.acceleratorForeground");
++
++		if (color == null) color = Color.black;
++
++		return color;
++	}
++
 +	public static boolean isDarkLaf()
 +	{
 +		return com.formdev.flatlaf.FlatLaf.isLafDark();
@@ -102,7 +113,7 @@
  	//{{{ getStyleString() method
  	/**
  	 * Converts a style into it's string representation.
-@@ -1619,6 +1641,21 @@
+@@ -1619,6 +1652,21 @@
  	}
  	//}}}
  
diff -r 782519a6ebb4 -r b47b65bd707f src/Tools/jEdit/patches/menu_accelerator
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/menu_accelerator	Wed Apr 23 14:54:06 2025 +0200
@@ -0,0 +1,144 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2025-04-23 14:40:22.714447724 +0200
+@@ -99,7 +99,7 @@
+ 
+ 		if(shortcut != null)
+ 		{
+-			FontMetrics fm = getFontMetrics(EnhancedMenuItem.acceleratorFont);
++			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
+ 			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
+ 		}
+ 		return d;
+@@ -114,11 +114,9 @@
+ 		if(shortcut != null)
+ 		{
+ 			Graphics2D g2 = (Graphics2D)g;
+-			g.setFont(EnhancedMenuItem.acceleratorFont);
++			g.setFont(GUIUtilities.menuAcceleratorFont());
+ 			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+-			g.setColor(getModel().isArmed() ?
+-				EnhancedMenuItem.acceleratorSelectionForeground :
+-				EnhancedMenuItem.acceleratorForeground);
++			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
+ 			FontMetrics fm = g.getFontMetrics();
+ 			Insets insets = getInsets();
+ 			g.drawString(shortcut,getWidth() - (fm.stringWidth(
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2025-04-23 14:26:16.757848751 +0200
+@@ -94,7 +94,7 @@
+ 
+ 		if(shortcut != null)
+ 		{
+-			FontMetrics fm = getFontMetrics(acceleratorFont);
++			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
+ 			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
+ 		}
+ 		return d;
+@@ -109,11 +109,9 @@
+ 		if(shortcut != null)
+ 		{
+ 			Graphics2D g2 = (Graphics2D)g;
+-			g.setFont(acceleratorFont);
++			g.setFont(GUIUtilities.menuAcceleratorFont());
+ 			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+-			g.setColor(getModel().isArmed() ?
+-				acceleratorSelectionForeground :
+-				acceleratorForeground);
++			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
+ 			FontMetrics fm = g.getFontMetrics();
+ 			Insets insets = getInsets();
+ 			g.drawString(shortcut,getWidth() - (fm.stringWidth(
+@@ -122,12 +120,6 @@
+ 		}
+ 	} //}}}
+ 
+-	//{{{ Package-private members
+-	static Font acceleratorFont;
+-	static Color acceleratorForeground;
+-	static Color acceleratorSelectionForeground;
+-	//}}}
+-
+ 	//{{{ Private members
+ 
+ 	//{{{ Instance variables
+@@ -135,25 +127,5 @@
+ 	private String shortcut;
+ 	//}}}
+ 
+-	//{{{ Class initializer
+-	static
+-	{
+-		acceleratorFont = GUIUtilities.menuAcceleratorFont();
+-
+-		acceleratorForeground = UIManager
+-			.getColor("MenuItem.acceleratorForeground");
+-		if(acceleratorForeground == null)
+-		{
+-			acceleratorForeground = Color.black;
+-		}
+-
+-		acceleratorSelectionForeground = UIManager
+-			.getColor("MenuItem.acceleratorSelectionForeground");
+-		if(acceleratorSelectionForeground == null)
+-		{
+-			acceleratorSelectionForeground = Color.black;
+-		}
+-	} //}}}
+-
+ 	//}}}
+ }
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2025-04-23 14:27:48.829375470 +0200
+@@ -107,7 +107,7 @@
+ 
+ 			if(shortcut != null)
+ 			{
+-				FontMetrics fm = getFontMetrics(acceleratorFont);
++				FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
+ 				d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
+ 			}
+ 			return d;
+@@ -124,11 +124,9 @@
+ 			if(shortcut != null)
+ 			{
+ 				Graphics2D g2 = (Graphics2D)g;
+-				g.setFont(acceleratorFont);
++				g.setFont(GUIUtilities.menuAcceleratorFont());
+ 				g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+-				g.setColor(getModel().isArmed() ?
+-					acceleratorSelectionForeground :
+-					acceleratorForeground);
++				g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
+ 				FontMetrics fm = g.getFontMetrics();
+ 				Insets insets = getInsets();
+ 				g.drawString(shortcut,getWidth() - (fm.stringWidth(
+@@ -140,9 +138,6 @@
+ 		//{{{ Private members
+ 		private final String shortcutProp;
+ 		private final char shortcut;
+-		private static final Font acceleratorFont;
+-		private static final Color acceleratorForeground;
+-		private static final Color acceleratorSelectionForeground;
+ 
+ 		//{{{ getShortcut() method
+ 		private String getShortcut()
+@@ -162,16 +157,6 @@
+ 			}
+ 		} //}}}
+ 
+-		//{{{ Class initializer
+-		static
+-		{
+-			acceleratorFont = GUIUtilities.menuAcceleratorFont();
+-			acceleratorForeground = UIManager
+-				.getColor("MenuItem.acceleratorForeground");
+-			acceleratorSelectionForeground = UIManager
+-				.getColor("MenuItem.acceleratorSelectionForeground");
+-		} //}}}
+-
+ 		//}}}
+ 	} //}}}
+ }