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 blanchet
Sun, 12 Oct 2014 21:52:44 +0200
changeset 58652 da12763acd6b
parent 53898 e4825d4c6bd7
child 59571 1081f91c0662
permissions -rw-r--r--
made SML/NJ happier
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 
     1
 
--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java	2013-07-28 19:03:38.000000000 +0200
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 
     2
 
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java	2013-09-10 21:55:21.220043663 +0200
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 
     3
 
@@ -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 
     4
 
 		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 
     5
 
 		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 
     6
 
 		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 
     7
 
-	/*	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 
     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_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 
    10
 
 		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 
    11
 
 		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 
    12
 
@@ -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 
    13
 
 		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 
    14
 
 		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 
    15
 
 		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 
    16
 
-		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 
    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_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 
    19
 
 		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 
    20
 
 		case KeyEvent.VK_DEAD_GRAVE:
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
 
@@ -202,28 +202,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 
    22
 
 	//{{{ 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 
    23
 
 	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 
    24
 
 	{
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
 
-		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 
    26
 
-		{
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
 
-		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 
    28
 
-		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 
    29
 
-		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 
    30
 
-		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 
    31
 
-		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 
    32
 
-		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 
    33
 
-		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 
    34
 
-		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 
    35
 
-		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 
    36
 
-		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 
    37
 
-		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 
    38
 
-		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 
    39
 
-		/* 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 
    40
 
-		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 
    41
 
-		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 
    42
 
-		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 
    43
 
-			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 
    44
 
-		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 
    45
 
-			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 
    46
 
-		}
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
 
+		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 
    48
 
 	} //}}}
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
 
 	//{{{ processKeyEvent() method
isabelle