src/Tools/jEdit/patches/menu_accelerator
changeset 82570 b47b65bd707f
child 83039 608973c627be
equal deleted inserted replaced
82569:782519a6ebb4 82570:b47b65bd707f
       
     1 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
       
     2 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2024-08-03 19:53:18.000000000 +0200
       
     3 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2025-04-23 14:40:22.714447724 +0200
       
     4 @@ -99,7 +99,7 @@
       
     5  
       
     6  		if(shortcut != null)
       
     7  		{
       
     8 -			FontMetrics fm = getFontMetrics(EnhancedMenuItem.acceleratorFont);
       
     9 +			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
       
    10  			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
       
    11  		}
       
    12  		return d;
       
    13 @@ -114,11 +114,9 @@
       
    14  		if(shortcut != null)
       
    15  		{
       
    16  			Graphics2D g2 = (Graphics2D)g;
       
    17 -			g.setFont(EnhancedMenuItem.acceleratorFont);
       
    18 +			g.setFont(GUIUtilities.menuAcceleratorFont());
       
    19  			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
       
    20 -			g.setColor(getModel().isArmed() ?
       
    21 -				EnhancedMenuItem.acceleratorSelectionForeground :
       
    22 -				EnhancedMenuItem.acceleratorForeground);
       
    23 +			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
       
    24  			FontMetrics fm = g.getFontMetrics();
       
    25  			Insets insets = getInsets();
       
    26  			g.drawString(shortcut,getWidth() - (fm.stringWidth(
       
    27 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
       
    28 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2024-08-03 19:53:18.000000000 +0200
       
    29 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2025-04-23 14:26:16.757848751 +0200
       
    30 @@ -94,7 +94,7 @@
       
    31  
       
    32  		if(shortcut != null)
       
    33  		{
       
    34 -			FontMetrics fm = getFontMetrics(acceleratorFont);
       
    35 +			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
       
    36  			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
       
    37  		}
       
    38  		return d;
       
    39 @@ -109,11 +109,9 @@
       
    40  		if(shortcut != null)
       
    41  		{
       
    42  			Graphics2D g2 = (Graphics2D)g;
       
    43 -			g.setFont(acceleratorFont);
       
    44 +			g.setFont(GUIUtilities.menuAcceleratorFont());
       
    45  			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
       
    46 -			g.setColor(getModel().isArmed() ?
       
    47 -				acceleratorSelectionForeground :
       
    48 -				acceleratorForeground);
       
    49 +			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
       
    50  			FontMetrics fm = g.getFontMetrics();
       
    51  			Insets insets = getInsets();
       
    52  			g.drawString(shortcut,getWidth() - (fm.stringWidth(
       
    53 @@ -122,12 +120,6 @@
       
    54  		}
       
    55  	} //}}}
       
    56  
       
    57 -	//{{{ Package-private members
       
    58 -	static Font acceleratorFont;
       
    59 -	static Color acceleratorForeground;
       
    60 -	static Color acceleratorSelectionForeground;
       
    61 -	//}}}
       
    62 -
       
    63  	//{{{ Private members
       
    64  
       
    65  	//{{{ Instance variables
       
    66 @@ -135,25 +127,5 @@
       
    67  	private String shortcut;
       
    68  	//}}}
       
    69  
       
    70 -	//{{{ Class initializer
       
    71 -	static
       
    72 -	{
       
    73 -		acceleratorFont = GUIUtilities.menuAcceleratorFont();
       
    74 -
       
    75 -		acceleratorForeground = UIManager
       
    76 -			.getColor("MenuItem.acceleratorForeground");
       
    77 -		if(acceleratorForeground == null)
       
    78 -		{
       
    79 -			acceleratorForeground = Color.black;
       
    80 -		}
       
    81 -
       
    82 -		acceleratorSelectionForeground = UIManager
       
    83 -			.getColor("MenuItem.acceleratorSelectionForeground");
       
    84 -		if(acceleratorSelectionForeground == null)
       
    85 -		{
       
    86 -			acceleratorSelectionForeground = Color.black;
       
    87 -		}
       
    88 -	} //}}}
       
    89 -
       
    90  	//}}}
       
    91  }
       
    92 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
       
    93 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2024-08-03 19:53:18.000000000 +0200
       
    94 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2025-04-23 14:27:48.829375470 +0200
       
    95 @@ -107,7 +107,7 @@
       
    96  
       
    97  			if(shortcut != null)
       
    98  			{
       
    99 -				FontMetrics fm = getFontMetrics(acceleratorFont);
       
   100 +				FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
       
   101  				d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
       
   102  			}
       
   103  			return d;
       
   104 @@ -124,11 +124,9 @@
       
   105  			if(shortcut != null)
       
   106  			{
       
   107  				Graphics2D g2 = (Graphics2D)g;
       
   108 -				g.setFont(acceleratorFont);
       
   109 +				g.setFont(GUIUtilities.menuAcceleratorFont());
       
   110  				g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
       
   111 -				g.setColor(getModel().isArmed() ?
       
   112 -					acceleratorSelectionForeground :
       
   113 -					acceleratorForeground);
       
   114 +				g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
       
   115  				FontMetrics fm = g.getFontMetrics();
       
   116  				Insets insets = getInsets();
       
   117  				g.drawString(shortcut,getWidth() - (fm.stringWidth(
       
   118 @@ -140,9 +138,6 @@
       
   119  		//{{{ Private members
       
   120  		private final String shortcutProp;
       
   121  		private final char shortcut;
       
   122 -		private static final Font acceleratorFont;
       
   123 -		private static final Color acceleratorForeground;
       
   124 -		private static final Color acceleratorSelectionForeground;
       
   125  
       
   126  		//{{{ getShortcut() method
       
   127  		private String getShortcut()
       
   128 @@ -162,16 +157,6 @@
       
   129  			}
       
   130  		} //}}}
       
   131  
       
   132 -		//{{{ Class initializer
       
   133 -		static
       
   134 -		{
       
   135 -			acceleratorFont = GUIUtilities.menuAcceleratorFont();
       
   136 -			acceleratorForeground = UIManager
       
   137 -				.getColor("MenuItem.acceleratorForeground");
       
   138 -			acceleratorSelectionForeground = UIManager
       
   139 -				.getColor("MenuItem.acceleratorSelectionForeground");
       
   140 -		} //}}}
       
   141 -
       
   142  		//}}}
       
   143  	} //}}}
       
   144  }