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 2024-10-29 11:50:54.062016616 +0100
@@ -1094,9 +1094,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();
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-11-15 18:42:41.560326356 +0100
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-11-15 20:33:52.458587638 +0100
@@ -1617,6 +1617,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()
{