diff -r 5945e5f4616e -r c6949c38cdd3 src/Tools/jEdit/patches/main --- a/src/Tools/jEdit/patches/main Sat Aug 23 18:54:22 2025 +0200 +++ b/src/Tools/jEdit/patches/main Sat Aug 23 20:10:58 2025 +0200 @@ -1359,10 +1359,10 @@ super.dispose(); } //}}} -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 +diff -Nru 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 2025-05-20 15:21:53.380719554 +0200 -@@ -53,6 +53,7 @@ ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2025-08-23 19:56:33.392876293 +0200 +@@ -53,11 +53,13 @@ import javax.swing.JComponent; import javax.swing.JPanel; import javax.swing.JPopupMenu; @@ -1370,7 +1370,13 @@ import javax.swing.JToggleButton; import javax.swing.UIManager; import javax.swing.border.Border; -@@ -99,7 +100,7 @@ + import javax.swing.border.EmptyBorder; + import javax.swing.plaf.metal.MetalLookAndFeel; ++import javax.accessibility.AccessibleContext; + + import org.gjt.sp.jedit.EditBus; + import org.gjt.sp.jedit.GUIUtilities; +@@ -99,7 +101,7 @@ closeBox.addActionListener(e -> show((DockableWindowManagerImpl.Entry)null)); @@ -1379,7 +1385,7 @@ menuBtn.setRequestFocusEnabled(false); menuBtn.setToolTipText(jEdit.getProperty("view.docking.menu-tooltip")); if(OperatingSystem.isMacOSLF()) -@@ -164,6 +165,7 @@ +@@ -164,11 +166,13 @@ { button = new JToggleButton(); button.setMargin(new Insets(1,1,1,1)); @@ -1387,7 +1393,15 @@ } GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6)); button.setRequestFocusEnabled(false); -@@ -683,8 +685,6 @@ +- button.setIcon(new RotatedTextIcon(rotation,button.getFont(), +- entry.shortTitle())); ++ String shortTitle = entry.shortTitle(); ++ button.setIcon(new RotatedTextIcon(rotation,button.getFont(), shortTitle)); ++ button.putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, shortTitle); + button.setActionCommand(entry.factory.name); + button.addActionListener(new ActionHandler()); + button.addMouseListener(new MenuMouseHandler()); +@@ -683,8 +687,6 @@ renderHints = new RenderingHints( RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);