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 haftmann
Wed, 24 Apr 2013 11:32:54 +0200
changeset 51750 cb154917a496
parent 50727 76ae4e6318fb
child 53415 9ebab8b7d73c
permissions -rw-r--r--
avoid odd reinit after sublocale declaration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset 
     1
 
diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset 
     2
 
--- 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java	2012-11-17 16:42:29.000000000 +0100
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset 
     3
 
+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java	2012-12-01 17:32:47.000000000 +0100
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset 
     4
 
@@ -318,6 +318,10 @@
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
     5
 
 			{
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset 
     6
 
 				os = WINDOWS_NT;
48786
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;
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset 
    15
 
diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
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 
    16
 
--- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java     2012-11-17 16:42:29.000000000 +0100
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 
    17
 
+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java     2013-01-04 20:00:25.698332853 +0100
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 
    18
 
@@ -109,7 +109,7 @@
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 
    19
 
         * used to handle a modifier key press in conjunction with an alphabet
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 
    20
 
         * key. <b>On by default on MacOS.</b>
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 
    21
 
         */
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 
    22
 
-       public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
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 
    23
 
+       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 
    24
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 
    25
 
        /**
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 
    26
 
         * If true, A+ shortcuts are disabled. If you use this, you should also
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 
    27
 
diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.0.0/jEdit-patched/org/gjt/sp/jed
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 
    28
 
it/gui/KeyEventWorkaround.java
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 
    29
 
--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java    2012-11-17 16:41:58.000000000 +0100
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 
    30
 
+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java    2013-01-04 20:04:43.02632209
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 
    31
 
2 +0100
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 
    32
 
@@ -297,8 +297,8 @@
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 
    33
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 
    34
 
                        if(!Debug.ALTERNATIVE_DISPATCHER)
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 
    35
 
                        {
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 
    36
 
-                               if(((modifiers & InputEvent.CTRL_MASK) != 0
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 
    37
 
-                                       ^ (modifiers & InputEvent.ALT_MASK) != 0)
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 
    38
 
+                               if((modifiers & InputEvent.CTRL_MASK) != 0 && (modifiers & InputEvent.ALT_MASK) == 0
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 
    39
 
+                                       || (modifiers & InputEvent.CTRL_MASK) == 0 && (modifiers & InputEvent.ALT_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED
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 
    40
 
                                        || (modifiers & InputEvent.META_MASK) != 0)
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 
    41
 
                                {
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 
    42
 
                                        return null;
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset 
    43
 














isabelle