--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/gui_utilities Wed Apr 23 13:32:16 2025 +0200
@@ -0,0 +1,126 @@
+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
+@@ -42,6 +42,8 @@
+ import java.net.URL;
+ import java.util.*;
+ import java.util.List;
++import java.util.regex.Pattern;
++import java.util.regex.Matcher;
+ import java.lang.ref.SoftReference;
+
+ import javax.annotation.Nonnull;
+@@ -72,6 +74,8 @@
+ import java.util.concurrent.ScheduledExecutorService;
+ import java.util.concurrent.TimeUnit;
+ import java.util.concurrent.atomic.AtomicLong;
++
++import com.formdev.flatlaf.extras.FlatSVGIcon;
+ //}}}
+
+ /** Various GUI utility functions related to icons, menus, toolbars, keyboard shortcuts, etc.
+@@ -115,14 +119,14 @@
+ * @return the icon
+ * @since jEdit 2.6pre7
+ */
+- public static Icon loadIcon(String iconName)
++ public static Icon loadIcon(String iconSpec)
+ {
+- if(iconName == null)
++ if(iconSpec == null)
+ return null;
+
+ // * Enable old icon naming scheme support
+- if(deprecatedIcons.containsKey(iconName))
+- iconName = deprecatedIcons.get(iconName);
++ if(deprecatedIcons.containsKey(iconSpec))
++ iconSpec = deprecatedIcons.get(iconSpec);
+
+ // check if there is a cached version first
+ Map<String, Icon> cache = null;
+@@ -135,12 +139,25 @@
+ cache = new HashMap<>();
+ iconCache = new SoftReference<>(cache);
+ }
+- Icon icon = cache.get(iconName);
++ Icon icon = cache.get(iconSpec);
+ if(icon != null)
+ return icon;
+
+ URL url;
+
++ float iconScale = 1.0f;
++ String iconName = iconSpec;
++ {
++ Matcher matcher = Pattern.compile("^([^?]+)\\?scale=(.+)$").matcher(iconSpec);
++ if (matcher.matches()) {
++ try {
++ iconScale = Float.valueOf(matcher.group(2));
++ iconName = matcher.group(1);
++ }
++ catch (NumberFormatException e) { }
++ }
++ }
++
+ try
+ {
+ // get the icon
+@@ -164,9 +181,11 @@
+ }
+ }
+
+- icon = new ImageIcon(url);
++ icon =
++ url.toString().endsWith(".svg") ?
++ new FlatSVGIcon(url).derive(iconScale) : new ImageIcon(url);
+
+- cache.put(iconName,icon);
++ cache.put(iconSpec,icon);
+ return icon;
+ } //}}}
+
+@@ -1094,9 +1113,7 @@
+ return new Font("Monospaced", Font.PLAIN, 12);
+ }
+ else {
+- Font font2 =
+- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
+- Font.PLAIN, font1.getSize());
++ Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
+ FontRenderContext frc = new FontRenderContext(null, true, false);
+ float scale =
+ font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
+@@ -1107,6 +1124,11 @@
+
+ //{{{ Colors and styles
+
++ public static boolean isDarkLaf()
++ {
++ return com.formdev.flatlaf.FlatLaf.isLafDark();
++ }
++
+ //{{{ getStyleString() method
+ /**
+ * Converts a style into it's string representation.
+@@ -1619,6 +1641,21 @@
+ }
+ //}}}
+
++ //{{{ isPopupTrigger() method
++ /**
++ * Returns if the specified event is the popup trigger event.
++ * This implements precisely defined behavior, as opposed to
++ * MouseEvent.isPopupTrigger().
++ * @param evt The event
++ * @since jEdit 3.2pre8
++ * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
++ */
++ @Deprecated
++ public static boolean isPopupTrigger(MouseEvent evt)
++ {
++ return GenericGUIUtilities.isPopupTrigger(evt);
++ } //}}}
++
+ //{{{ init() method
+ static void init()
+ {
--- a/src/Tools/jEdit/patches/icons Wed Apr 23 10:01:34 2025 +0200
+++ b/src/Tools/jEdit/patches/icons Wed Apr 23 13:32:16 2025 +0200
@@ -29,87 +29,6 @@
+ <dependency org="com.formdev" name="flatlaf-extras" rev="3.6"/>
</dependencies>
</ivy-module>
-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-16 12:21:09.744865617 +0200
-@@ -42,6 +42,8 @@
- import java.net.URL;
- import java.util.*;
- import java.util.List;
-+import java.util.regex.Pattern;
-+import java.util.regex.Matcher;
- import java.lang.ref.SoftReference;
-
- import javax.annotation.Nonnull;
-@@ -72,6 +74,8 @@
- import java.util.concurrent.ScheduledExecutorService;
- import java.util.concurrent.TimeUnit;
- import java.util.concurrent.atomic.AtomicLong;
-+
-+import com.formdev.flatlaf.extras.FlatSVGIcon;
- //}}}
-
- /** Various GUI utility functions related to icons, menus, toolbars, keyboard shortcuts, etc.
-@@ -115,14 +119,14 @@
- * @return the icon
- * @since jEdit 2.6pre7
- */
-- public static Icon loadIcon(String iconName)
-+ public static Icon loadIcon(String iconSpec)
- {
-- if(iconName == null)
-+ if(iconSpec == null)
- return null;
-
- // * Enable old icon naming scheme support
-- if(deprecatedIcons.containsKey(iconName))
-- iconName = deprecatedIcons.get(iconName);
-+ if(deprecatedIcons.containsKey(iconSpec))
-+ iconSpec = deprecatedIcons.get(iconSpec);
-
- // check if there is a cached version first
- Map<String, Icon> cache = null;
-@@ -135,12 +139,25 @@
- cache = new HashMap<>();
- iconCache = new SoftReference<>(cache);
- }
-- Icon icon = cache.get(iconName);
-+ Icon icon = cache.get(iconSpec);
- if(icon != null)
- return icon;
-
- URL url;
-
-+ float iconScale = 1.0f;
-+ String iconName = iconSpec;
-+ {
-+ Matcher matcher = Pattern.compile("^([^?]+)\\?scale=(.+)$").matcher(iconSpec);
-+ if (matcher.matches()) {
-+ try {
-+ iconScale = Float.valueOf(matcher.group(2));
-+ iconName = matcher.group(1);
-+ }
-+ catch (NumberFormatException e) { }
-+ }
-+ }
-+
- try
- {
- // get the icon
-@@ -164,9 +181,11 @@
- }
- }
-
-- icon = new ImageIcon(url);
-+ icon =
-+ url.toString().endsWith(".svg") ?
-+ new FlatSVGIcon(url).derive(iconScale) : new ImageIcon(url);
-
-- cache.put(iconName,icon);
-+ cache.put(iconSpec,icon);
- return icon;
- } //}}}
-
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java 2025-04-16 21:35:23.519418287 +0200
--- a/src/Tools/jEdit/patches/menus_and_sidekick Wed Apr 23 10:01:34 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-08-03 19:53:16.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-11-15 20:22:26.451538237 +0100
-@@ -225,8 +225,11 @@
- else
- this.message.setText(" ");
- }
-- else
-- this.message.setText(message);
-+ else {
-+ Exception exn = new Exception();
-+ if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
-+ this.message.setText(message);
-+ }
- } //}}}
-
- //{{{ setMessageComponent() method
-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 17:29:21.807286585 +0200
-@@ -1094,9 +1113,7 @@
- return new Font("Monospaced", Font.PLAIN, 12);
- }
- else {
-- Font font2 =
-- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
-- Font.PLAIN, font1.getSize());
-+ Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
- FontRenderContext frc = new FontRenderContext(null, true, false);
- float scale =
- font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
-@@ -1107,6 +1124,11 @@
-
- //{{{ Colors and styles
-
-+ public static boolean isDarkLaf()
-+ {
-+ return com.formdev.flatlaf.FlatLaf.isLafDark();
-+ }
-+
- //{{{ getStyleString() method
- /**
- * Converts a style into it's string representation.
-@@ -1619,6 +1641,21 @@
- }
- //}}}
-
-+ //{{{ isPopupTrigger() method
-+ /**
-+ * Returns if the specified event is the popup trigger event.
-+ * This implements precisely defined behavior, as opposed to
-+ * MouseEvent.isPopupTrigger().
-+ * @param evt The event
-+ * @since jEdit 3.2pre8
-+ * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
-+ */
-+ @Deprecated
-+ public static boolean isPopupTrigger(MouseEvent evt)
-+ {
-+ return GenericGUIUtilities.isPopupTrigger(evt);
-+ } //}}}
-+
- //{{{ init() method
- static void init()
- {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/status_bar Wed Apr 23 13:32:16 2025 +0200
@@ -0,0 +1,17 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-11-15 20:22:26.451538237 +0100
+@@ -225,8 +225,11 @@
+ else
+ this.message.setText(" ");
+ }
+- else
+- this.message.setText(message);
++ else {
++ Exception exn = new Exception();
++ if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
++ this.message.setText(message);
++ }
+ } //}}}
+
+ //{{{ setMessageComponent() method