src/Tools/jEdit/patches/main
changeset 83042 c6949c38cdd3
parent 83041 5945e5f4616e
child 83049 835ea41cdc43
--- 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);