|
1 --- 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-07-28 19:03:38.000000000 +0200 |
|
2 +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-09-10 21:55:21.220043663 +0200 |
|
3 @@ -129,7 +129,7 @@ |
|
4 case KeyEvent.VK_OPEN_BRACKET : |
|
5 case KeyEvent.VK_BACK_SLASH : |
|
6 case KeyEvent.VK_CLOSE_BRACKET: |
|
7 - /* case KeyEvent.VK_NUMPAD0 : |
|
8 + case KeyEvent.VK_NUMPAD0 : |
|
9 case KeyEvent.VK_NUMPAD1 : |
|
10 case KeyEvent.VK_NUMPAD2 : |
|
11 case KeyEvent.VK_NUMPAD3 : |
|
12 @@ -144,7 +144,7 @@ |
|
13 case KeyEvent.VK_SEPARATOR: |
|
14 case KeyEvent.VK_SUBTRACT : |
|
15 case KeyEvent.VK_DECIMAL : |
|
16 - case KeyEvent.VK_DIVIDE :*/ |
|
17 + case KeyEvent.VK_DIVIDE : |
|
18 case KeyEvent.VK_BACK_QUOTE: |
|
19 case KeyEvent.VK_QUOTE: |
|
20 case KeyEvent.VK_DEAD_GRAVE: |
|
21 @@ -202,28 +202,7 @@ |
|
22 //{{{ isNumericKeypad() method |
|
23 public static boolean isNumericKeypad(int keyCode) |
|
24 { |
|
25 - switch(keyCode) |
|
26 - { |
|
27 - case KeyEvent.VK_NUMPAD0: |
|
28 - case KeyEvent.VK_NUMPAD1: |
|
29 - case KeyEvent.VK_NUMPAD2: |
|
30 - case KeyEvent.VK_NUMPAD3: |
|
31 - case KeyEvent.VK_NUMPAD4: |
|
32 - case KeyEvent.VK_NUMPAD5: |
|
33 - case KeyEvent.VK_NUMPAD6: |
|
34 - case KeyEvent.VK_NUMPAD7: |
|
35 - case KeyEvent.VK_NUMPAD8: |
|
36 - case KeyEvent.VK_NUMPAD9: |
|
37 - case KeyEvent.VK_MULTIPLY: |
|
38 - case KeyEvent.VK_ADD: |
|
39 - /* case KeyEvent.VK_SEPARATOR: */ |
|
40 - case KeyEvent.VK_SUBTRACT: |
|
41 - case KeyEvent.VK_DECIMAL: |
|
42 - case KeyEvent.VK_DIVIDE: |
|
43 - return true; |
|
44 - default: |
|
45 - return false; |
|
46 - } |
|
47 + return false; |
|
48 } //}}} |
|
49 |
|
50 //{{{ processKeyEvent() method |