Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/menu_accelerator
author nipkow
Tue, 17 Jun 2025 14:11:40 +0200
changeset 82733 8b537e1af2ec
parent 82570 b47b65bd707f
permissions -rw-r--r--
reinstated intersection of lists as inter_list_set
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
82570
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     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
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     2
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2024-08-03 19:53:18.000000000 +0200
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     3
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedCheckBoxMenuItem.java	2025-04-23 14:40:22.714447724 +0200
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     4
 
@@ -99,7 +99,7 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     5
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     6
 
 		if(shortcut != null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     7
 
 		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     8
 
-			FontMetrics fm = getFontMetrics(EnhancedMenuItem.acceleratorFont);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
     9
 
+			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    10
 
 			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    11
 
 		}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    12
 
 		return d;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    13
 
@@ -114,11 +114,9 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    14
 
 		if(shortcut != null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    15
 
 		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    16
 
 			Graphics2D g2 = (Graphics2D)g;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    17
 
-			g.setFont(EnhancedMenuItem.acceleratorFont);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    18
 
+			g.setFont(GUIUtilities.menuAcceleratorFont());
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    19
 
 			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    20
 
-			g.setColor(getModel().isArmed() ?
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    21
 
-				EnhancedMenuItem.acceleratorSelectionForeground :
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    22
 
-				EnhancedMenuItem.acceleratorForeground);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    23
 
+			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    24
 
 			FontMetrics fm = g.getFontMetrics();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    25
 
 			Insets insets = getInsets();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    26
 
 			g.drawString(shortcut,getWidth() - (fm.stringWidth(
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    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
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    28
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2024-08-03 19:53:18.000000000 +0200
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    29
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/EnhancedMenuItem.java	2025-04-23 14:26:16.757848751 +0200
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    30
 
@@ -94,7 +94,7 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    31
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    32
 
 		if(shortcut != null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    33
 
 		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    34
 
-			FontMetrics fm = getFontMetrics(acceleratorFont);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    35
 
+			FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    36
 
 			d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    37
 
 		}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    38
 
 		return d;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    39
 
@@ -109,11 +109,9 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    40
 
 		if(shortcut != null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    41
 
 		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    42
 
 			Graphics2D g2 = (Graphics2D)g;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    43
 
-			g.setFont(acceleratorFont);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    44
 
+			g.setFont(GUIUtilities.menuAcceleratorFont());
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    45
 
 			g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    46
 
-			g.setColor(getModel().isArmed() ?
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    47
 
-				acceleratorSelectionForeground :
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    48
 
-				acceleratorForeground);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    49
 
+			g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    50
 
 			FontMetrics fm = g.getFontMetrics();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    51
 
 			Insets insets = getInsets();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    52
 
 			g.drawString(shortcut,getWidth() - (fm.stringWidth(
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    53
 
@@ -122,12 +120,6 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    54
 
 		}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    55
 
 	} //}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    56
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    57
 
-	//{{{ Package-private members
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    58
 
-	static Font acceleratorFont;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    59
 
-	static Color acceleratorForeground;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    60
 
-	static Color acceleratorSelectionForeground;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    61
 
-	//}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    62
 
-
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    63
 
 	//{{{ Private members
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    64
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    65
 
 	//{{{ Instance variables
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    66
 
@@ -135,25 +127,5 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    67
 
 	private String shortcut;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    68
 
 	//}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    69
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    70
 
-	//{{{ Class initializer
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    71
 
-	static
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    72
 
-	{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    73
 
-		acceleratorFont = GUIUtilities.menuAcceleratorFont();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    74
 
-
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    75
 
-		acceleratorForeground = UIManager
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    76
 
-			.getColor("MenuItem.acceleratorForeground");
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    77
 
-		if(acceleratorForeground == null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    78
 
-		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    79
 
-			acceleratorForeground = Color.black;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    80
 
-		}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    81
 
-
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    82
 
-		acceleratorSelectionForeground = UIManager
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    83
 
-			.getColor("MenuItem.acceleratorSelectionForeground");
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    84
 
-		if(acceleratorSelectionForeground == null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    85
 
-		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    86
 
-			acceleratorSelectionForeground = Color.black;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    87
 
-		}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    88
 
-	} //}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    89
 
-
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    90
 
 	//}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    91
 
 }
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    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
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    93
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2024-08-03 19:53:18.000000000 +0200
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    94
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/MarkersProvider.java	2025-04-23 14:27:48.829375470 +0200
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    95
 
@@ -107,7 +107,7 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    96
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    97
 
 			if(shortcut != null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    98
 
 			{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
    99
 
-				FontMetrics fm = getFontMetrics(acceleratorFont);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   100
 
+				FontMetrics fm = getFontMetrics(GUIUtilities.menuAcceleratorFont());
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   101
 
 				d.width += (fm.stringWidth(shortcut) + fm.stringWidth("AAAA"));
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   102
 
 			}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   103
 
 			return d;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   104
 
@@ -124,11 +124,9 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   105
 
 			if(shortcut != null)
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   106
 
 			{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   107
 
 				Graphics2D g2 = (Graphics2D)g;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   108
 
-				g.setFont(acceleratorFont);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   109
 
+				g.setFont(GUIUtilities.menuAcceleratorFont());
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   110
 
 				g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   111
 
-				g.setColor(getModel().isArmed() ?
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   112
 
-					acceleratorSelectionForeground :
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   113
 
-					acceleratorForeground);
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   114
 
+				g.setColor(GUIUtilities.menuAcceleratorForeground(getModel().isArmed()));
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   115
 
 				FontMetrics fm = g.getFontMetrics();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   116
 
 				Insets insets = getInsets();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   117
 
 				g.drawString(shortcut,getWidth() - (fm.stringWidth(
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   118
 
@@ -140,9 +138,6 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   119
 
 		//{{{ Private members
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   120
 
 		private final String shortcutProp;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   121
 
 		private final char shortcut;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   122
 
-		private static final Font acceleratorFont;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   123
 
-		private static final Color acceleratorForeground;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   124
 
-		private static final Color acceleratorSelectionForeground;
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   125
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   126
 
 		//{{{ getShortcut() method
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   127
 
 		private String getShortcut()
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   128
 
@@ -162,16 +157,6 @@
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   129
 
 			}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   130
 
 		} //}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   131
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   132
 
-		//{{{ Class initializer
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   133
 
-		static
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   134
 
-		{
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   135
 
-			acceleratorFont = GUIUtilities.menuAcceleratorFont();
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   136
 
-			acceleratorForeground = UIManager
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   137
 
-				.getColor("MenuItem.acceleratorForeground");
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   138
 
-			acceleratorSelectionForeground = UIManager
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   139
 
-				.getColor("MenuItem.acceleratorSelectionForeground");
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   140
 
-		} //}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   141
 
-
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   142
 
 		//}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   143
 
 	} //}}}
b47b65bd707f proper painting of menu accelerator in dark mode;
wenzelm
parents:
diff changeset 
   144
 
 }
isabelle