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/jedit-4.5.2/macos
author wenzelm
Mon, 13 Aug 2012 19:51:48 +0200
changeset 48787 ab3e7f40f341
parent 48786 2b08d10a2f75
permissions -rw-r--r--
fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     1
 
diff -ru jEdit/org/gjt/sp/jedit/OperatingSystem.java jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     2
 
--- jEdit/org/gjt/sp/jedit/OperatingSystem.java	2012-06-15 22:20:24.000000000 +0200
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     3
 
+++ jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java	2012-08-13 19:13:06.000000000 +0200
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     4
 
@@ -317,6 +317,10 @@
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     5
 
 			{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     6
 
 				os = OS2;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     7
 
 			}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     8
 
+			else if(osName.contains("Mac OS X"))
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     9
 
+			{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    10
 
+				os = MAC_OS_X;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    11
 
+			}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    12
 
 			else if(osName.contains("VMS"))
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    13
 
 			{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    14
 
 				os = VMS;
48787
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    15
 
diff -ru jEdit/org/gjt/sp/jedit/Debug.java jEdit-patched/org/gjt/sp/jedit/Debug.java
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    16
 
--- jEdit/org/gjt/sp/jedit/Debug.java	2012-06-15 22:20:24.000000000 +0200
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    17
 
+++ jEdit-patched/org/gjt/sp/jedit/Debug.java	2012-08-13 19:44:43.000000000 +0200
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    18
 
@@ -109,7 +109,8 @@
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    19
 
 	 * used to handle a modifier key press in conjunction with an alphabet
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    20
 
 	 * key. <b>On by default on MacOS.</b>
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    21
 
 	 */
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    22
 
-	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    23
 
+	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS() &&
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    24
 
+		System.getProperty("java.version").startsWith("1.6.");
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    25
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    26
 
 	/**
ab3e7f40f341 fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
wenzelm
parents: 48786
diff changeset 
    27
 
 	 * If true, A+ shortcuts are disabled. If you use this, you should also
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    28
 














isabelle