leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6;
authorwenzelm
Sat, 01 Dec 2012 22:23:42 +0100
changeset 50307 6f64ce2e5a40
parent 50306 b655d2d0406d
child 50308 08b55c5ce064
leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6;
src/Tools/jEdit/patches/jedit/macos
--- a/src/Tools/jEdit/patches/jedit/macos	Sat Dec 01 19:51:43 2012 +0100
+++ b/src/Tools/jEdit/patches/jedit/macos	Sat Dec 01 22:23:42 2012 +0100
@@ -14,15 +14,25 @@
  				os = VMS;
 diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
 --- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java	2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java	2012-12-01 17:31:24.000000000 +0100
-@@ -109,7 +109,8 @@
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java	2012-12-01 21:55:48.000000000 +0100
+@@ -109,6 +109,7 @@
  	 * used to handle a modifier key press in conjunction with an alphabet
  	 * key. <b>On by default on MacOS.</b>
  	 */
--	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
-+	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS() &&
-+		System.getProperty("java.version").startsWith("1.6.");
++	public static boolean ALTERNATIVE_DISPATCHER0 = false;
+ 	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
  
  	/**
- 	 * If true, A+ shortcuts are disabled. If you use this, you should also
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventTranslator.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventTranslator.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventTranslator.java	2012-11-17 16:41:58.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventTranslator.java	2012-12-01 21:56:04.000000000 +0100
+@@ -79,7 +79,7 @@
+ 				|| (keyCode >= KeyEvent.VK_A
+ 				&& keyCode <= KeyEvent.VK_Z))
+ 			{
+-				if(Debug.ALTERNATIVE_DISPATCHER)
++				if(Debug.ALTERNATIVE_DISPATCHER0)
+ 					return null;
+ 				else
+ 				{