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/macos
author wenzelm
Thu, 05 Sep 2013 12:33:51 +0200
changeset 53415 9ebab8b7d73c
parent 50727 76ae4e6318fb
permissions -rw-r--r--
updated to jedit_build-20130905 which is based on jedit-5.1.0; added jsr305-2.0.0.jar from http://code.google.com/p/findbugs (via ivy cache), which is required to resolve javax.annotation.*;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53415
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     1
 
diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     2
 
--- 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java	2013-07-28 19:03:49.000000000 +0200
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     3
 
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java	2013-09-05 10:55:36.388181955 +0200
50727
76ae4e6318fb another attempt to get Mac OS X keyhandling right: ALTERNATIVE_DISPATCHER is off, but ALT_KEY_PRESSED_DISABLED is more careful to interpret ALT like ALT_GRAPH, which does not count as modifier here (NB: CONTROL + ALT means ALT_GRAPH on Windows, but ALT means ALT_GRAPH on Mac OS X);
wenzelm
parents: 50307
diff changeset 
     4
 
@@ -109,7 +109,7 @@
53415
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     5
 
 	 * used to handle a modifier key press in conjunction with an alphabet
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     6
 
 	 * key. <b>On by default on MacOS.</b>
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     7
 
 	 */
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     8
 
-	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
     9
 
+	public static boolean ALTERNATIVE_DISPATCHER = false;
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 
    10
53415
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
    11
 
 	/**
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 50727
diff changeset 
    12
 
 	 * 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 
    13
 














isabelle