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/numeric_keypad
author hoelzl
Mon, 13 Apr 2015 12:15:29 +0200
changeset 60045 cd2b6debac18
parent 59571 1081f91c0662
permissions -rw-r--r--
predicate compiler: ignore Abs_filter and Rep_filter
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59571
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 53898
diff changeset 
     1
 
diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 53898
diff changeset 
     2
 
--- 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java	2015-02-02 02:14:28.000000000 +0100
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 53898
diff changeset 
     3
 
+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java	2015-02-28 20:56:06.676244609 +0100
53521
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
     4
 
@@ -129,7 +129,7 @@
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
     5
 
 		case KeyEvent.VK_OPEN_BRACKET :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
     6
 
 		case KeyEvent.VK_BACK_SLASH   :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
     7
 
 		case KeyEvent.VK_CLOSE_BRACKET:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
     8
 
-	/*	case KeyEvent.VK_NUMPAD0 :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
     9
 
+		case KeyEvent.VK_NUMPAD0 :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    10
 
 		case KeyEvent.VK_NUMPAD1 :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    11
 
 		case KeyEvent.VK_NUMPAD2 :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    12
 
 		case KeyEvent.VK_NUMPAD3 :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    13
 
@@ -144,7 +144,7 @@
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    14
 
 		case KeyEvent.VK_SEPARATOR:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    15
 
 		case KeyEvent.VK_SUBTRACT   :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    16
 
 		case KeyEvent.VK_DECIMAL    :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    17
 
-		case KeyEvent.VK_DIVIDE     :*/
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    18
 
+		case KeyEvent.VK_DIVIDE     :
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    19
 
 		case KeyEvent.VK_BACK_QUOTE:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    20
 
 		case KeyEvent.VK_QUOTE:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    21
 
 		case KeyEvent.VK_DEAD_GRAVE:
59571
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 53898
diff changeset 
    22
 
@@ -191,28 +191,7 @@
53521
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    23
 
 	//{{{ isNumericKeypad() method
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    24
 
 	public static boolean isNumericKeypad(int keyCode)
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    25
 
 	{
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    26
 
-		switch(keyCode)
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    27
 
-		{
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    28
 
-		case KeyEvent.VK_NUMPAD0:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    29
 
-		case KeyEvent.VK_NUMPAD1:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    30
 
-		case KeyEvent.VK_NUMPAD2:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    31
 
-		case KeyEvent.VK_NUMPAD3:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    32
 
-		case KeyEvent.VK_NUMPAD4:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    33
 
-		case KeyEvent.VK_NUMPAD5:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    34
 
-		case KeyEvent.VK_NUMPAD6:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    35
 
-		case KeyEvent.VK_NUMPAD7:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    36
 
-		case KeyEvent.VK_NUMPAD8:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    37
 
-		case KeyEvent.VK_NUMPAD9:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    38
 
-		case KeyEvent.VK_MULTIPLY:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    39
 
-		case KeyEvent.VK_ADD:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    40
 
-		/* case KeyEvent.VK_SEPARATOR: */
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    41
 
-		case KeyEvent.VK_SUBTRACT:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    42
 
-		case KeyEvent.VK_DECIMAL:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    43
 
-		case KeyEvent.VK_DIVIDE:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    44
 
-			return true;
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    45
 
-		default:
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    46
 
-			return false;
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    47
 
-		}
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    48
 
+		return false;
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    49
 
 	} //}}}
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    50
2a64cae5e611 disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
wenzelm
parents:
diff changeset 
    51
 
 	//{{{ processKeyEvent() method
isabelle