Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/menus_and_sidekick
author wenzelm
Sun, 17 Nov 2024 13:57:50 +0100
changeset 81474 a3dc66165d15
parent 81454 0bdb0d8e50c0
child 82560 ea65da20d173
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73653
diff changeset 
     1
 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73653
diff changeset 
     2
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-08-03 19:53:15.000000000 +0200
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73653
diff changeset 
     3
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-10-29 11:50:54.062016616 +0100
07f64697408e update to jedit5.7.0;
wenzelm
parents: 73653
diff changeset 
     4
 
@@ -1094,9 +1094,7 @@
69382
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
     5
 
 				return new Font("Monospaced", Font.PLAIN, 12);
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
     6
 
 			}
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
     7
 
 			else {
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
     8
 
-				Font font2 =
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
     9
 
-					new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
    10
 
-						Font.PLAIN, font1.getSize());
69382
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
    11
 
+				Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
    12
 
 				FontRenderContext frc = new FontRenderContext(null, true, false);
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
    13
 
 				float scale =
d70767e508d7 proper menu accelerator font for Java 11 (no update of jedit-build component yet);
wenzelm
parents:
diff changeset 
    14
 
 					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
81454
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    15
 
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
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    16
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-08-03 19:53:16.000000000 +0200
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    17
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java	2024-11-15 20:22:26.451538237 +0100
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    18
 
@@ -225,8 +225,11 @@
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    19
 
 			else
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    20
 
 				this.message.setText(" ");
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    21
 
 		}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    22
 
-		else
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    23
 
-			this.message.setText(message);
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    24
 
+		else {
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    25
 
+			Exception exn = new Exception();
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    26
 
+			if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    27
 
+				this.message.setText(message);
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    28
 
+		}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    29
 
 	} //}}}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    30
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    31
 
 	//{{{ setMessageComponent() method
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    32
 
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    33
 
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-11-15 18:42:41.560326356 +0100
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    34
 
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-11-15 20:33:52.458587638 +0100
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    35
 
@@ -1617,6 +1617,21 @@
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    36
 
 	}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    37
 
 	//}}}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    38
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    39
 
+	//{{{ isPopupTrigger() method
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    40
 
+	/**
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    41
 
+	 * Returns if the specified event is the popup trigger event.
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    42
 
+	 * This implements precisely defined behavior, as opposed to
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    43
 
+	 * MouseEvent.isPopupTrigger().
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    44
 
+	 * @param evt The event
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    45
 
+	 * @since jEdit 3.2pre8
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    46
 
+	 * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    47
 
+	 */
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    48
 
+	@Deprecated
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    49
 
+	public static boolean isPopupTrigger(MouseEvent evt)
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    50
 
+	{
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    51
 
+		return GenericGUIUtilities.isPopupTrigger(evt);
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    52
 
+	} //}}}
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    53
 
+
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    54
 
 	//{{{ init() method
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    55
 
 	static void init()
0bdb0d8e50c0 more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
wenzelm
parents: 81297
diff changeset 
    56
 
 	{
isabelle