1 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 |
|
2 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-08-03 19:53:16.000000000 +0200 |
|
3 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-11-15 20:22:26.451538237 +0100 |
|
4 @@ -225,8 +225,11 @@ |
|
5 else |
|
6 this.message.setText(" "); |
|
7 } |
|
8 - else |
|
9 - this.message.setText(message); |
|
10 + else { |
|
11 + Exception exn = new Exception(); |
|
12 + if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick.")) |
|
13 + this.message.setText(message); |
|
14 + } |
|
15 } //}}} |
|
16 |
|
17 //{{{ setMessageComponent() method |
|
18 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java |
|
19 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200 |
|
20 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-04-22 17:29:21.807286585 +0200 |
|
21 @@ -1094,9 +1113,7 @@ |
|
22 return new Font("Monospaced", Font.PLAIN, 12); |
|
23 } |
|
24 else { |
|
25 - Font font2 = |
|
26 - new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced", |
|
27 - Font.PLAIN, font1.getSize()); |
|
28 + Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize()); |
|
29 FontRenderContext frc = new FontRenderContext(null, true, false); |
|
30 float scale = |
|
31 font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight(); |
|
32 @@ -1107,6 +1124,11 @@ |
|
33 |
|
34 //{{{ Colors and styles |
|
35 |
|
36 + public static boolean isDarkLaf() |
|
37 + { |
|
38 + return com.formdev.flatlaf.FlatLaf.isLafDark(); |
|
39 + } |
|
40 + |
|
41 //{{{ getStyleString() method |
|
42 /** |
|
43 * Converts a style into it's string representation. |
|
44 @@ -1619,6 +1641,21 @@ |
|
45 } |
|
46 //}}} |
|
47 |
|
48 + //{{{ isPopupTrigger() method |
|
49 + /** |
|
50 + * Returns if the specified event is the popup trigger event. |
|
51 + * This implements precisely defined behavior, as opposed to |
|
52 + * MouseEvent.isPopupTrigger(). |
|
53 + * @param evt The event |
|
54 + * @since jEdit 3.2pre8 |
|
55 + * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)} |
|
56 + */ |
|
57 + @Deprecated |
|
58 + public static boolean isPopupTrigger(MouseEvent evt) |
|
59 + { |
|
60 + return GenericGUIUtilities.isPopupTrigger(evt); |
|
61 + } //}}} |
|
62 + |
|
63 //{{{ init() method |
|
64 static void init() |
|
65 { |
|