# HG changeset patch # User wenzelm # Date 1745407936 -7200 # Node ID 782519a6ebb48645258a5d91e202168c3c076c41 # Parent f35e82124b3349de89c94c0f9df2b60a38033382 clarified patches; diff -r f35e82124b33 -r 782519a6ebb4 src/Tools/jEdit/patches/gui_utilities --- /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 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() + { diff -r f35e82124b33 -r 782519a6ebb4 src/Tools/jEdit/patches/icons --- 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 @@ + -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 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 diff -r f35e82124b33 -r 782519a6ebb4 src/Tools/jEdit/patches/menus_and_sidekick --- 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() - { diff -r f35e82124b33 -r 782519a6ebb4 src/Tools/jEdit/patches/status_bar --- /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