--- a/Admin/components/components.sha1 Wed Apr 23 13:32:16 2025 +0200
+++ b/Admin/components/components.sha1 Wed Apr 23 14:54:06 2025 +0200
@@ -273,6 +273,7 @@
cab6dca89dc2e0d922e92cc47df07941a3c6b29c jedit-20250415.tar.gz
23297ab36a853247a17f87b94a29654f3259b341 jedit-20250417.tar.gz
a291746959e64916e8504b89dca804186d4eb8a1 jedit-20250422.tar.gz
+07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Wed Apr 23 13:32:16 2025 +0200
+++ b/Admin/components/main Wed Apr 23 14:54:06 2025 +0200
@@ -15,7 +15,7 @@
isabelle_setup-20240327
javamail-20250122
jdk-21.0.6
-jedit-20250422
+jedit-20250423
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.18.3
--- a/src/Tools/jEdit/patches/gui_utilities Wed Apr 23 13:32:16 2025 +0200
+++ b/src/Tools/jEdit/patches/gui_utilities Wed Apr 23 14:54:06 2025 +0200
@@ -1,6 +1,6 @@
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-04-22 22:11:53.770185212 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-04-23 14:28:53.149349418 +0200
@@ -42,6 +42,8 @@
import java.net.URL;
import java.util.*;
@@ -90,10 +90,21 @@
FontRenderContext frc = new FontRenderContext(null, true, false);
float scale =
font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
-@@ -1107,6 +1124,11 @@
+@@ -1107,6 +1124,22 @@
//{{{ Colors and styles
++ public static Color menuAcceleratorForeground(boolean selection) {
++ Color color =
++ UIManager.getColor(selection ?
++ "MenuItem.acceleratorSelectionForeground" :
++ "MenuItem.acceleratorForeground");
++
++ if (color == null) color = Color.black;
++
++ return color;
++ }
++
+ public static boolean isDarkLaf()
+ {
+ return com.formdev.flatlaf.FlatLaf.isLafDark();
@@ -102,7 +113,7 @@
//{{{ getStyleString() method
/**
* Converts a style into it's string representation.
-@@ -1619,6 +1641,21 @@
+@@ -1619,6 +1652,21 @@
}
//}}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/menu_accelerator Wed Apr 23 14:54:06 2025 +0200
@@ -0,0 +1,144 @@
+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 -ru 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-04-23 14:26:16.757848751 +0200
+@@ -94,7 +94,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 +109,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 +120,6 @@
+ }
+ } //}}}
+
+- //{{{ Package-private members
+- static Font acceleratorFont;
+- static Color acceleratorForeground;
+- static Color acceleratorSelectionForeground;
+- //}}}
+-
+ //{{{ Private members
+
+ //{{{ Instance variables
+@@ -135,25 +127,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");
+- } //}}}
+-
+ //}}}
+ } //}}}
+ }