Quelle  menu_accelerator

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 -Nru 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-08-23 17:10:11.503674580 +0200
@@ -30,6 +30,7 @@
 import org.gjt.sp.jedit.gui.KeyEventTranslator;
 import org.gjt.sp.jedit.gui.statusbar.HoverSetStatusMouseHandler;
 import org.jedit.keymap.Keymap;
+import javax.accessibility.AccessibleContext;
 //}}}
 
 /**
@@ -54,11 +55,14 @@
    setToolTipText(toolTip);
   }
 
+  if (shortcut != null)
+   putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, label + " (" + shortcut + ")");
+
   if (OperatingSystem.hasScreenMenuBar() && shortcut != null)
   {
    if (jEdit.getBooleanProperty("menu.multiShortcut", false))
    {
-    setText(label + " ( " + shortcut + " )");
+    setText(label + " (" + shortcut + ")");
    }
    else
    {
@@ -94,7 +98,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 +113,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 +124,6 @@
   }
  } //}}}
 
- //{{{ Package-private members
- static Font acceleratorFont;
- static Color acceleratorForeground;
- static Color acceleratorSelectionForeground;
- //}}}
-
  //{{{ Private members
 
  //{{{ Instance variables
@@ -135,25 +131,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");
-  } //}}}
-
   //}}}
  } //}}}
 }