--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-07-28 19:03:38.000000000 +0200
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-09-10 21:55:21.220043663 +0200
@@ -129,7 +129,7 @@
case KeyEvent.VK_OPEN_BRACKET :
case KeyEvent.VK_BACK_SLASH :
case KeyEvent.VK_CLOSE_BRACKET:
- /* case KeyEvent.VK_NUMPAD0 :
+ case KeyEvent.VK_NUMPAD0 :
case KeyEvent.VK_NUMPAD1 :
case KeyEvent.VK_NUMPAD2 :
case KeyEvent.VK_NUMPAD3 :
@@ -144,7 +144,7 @@
case KeyEvent.VK_SEPARATOR:
case KeyEvent.VK_SUBTRACT :
case KeyEvent.VK_DECIMAL :
- case KeyEvent.VK_DIVIDE :*/
+ case KeyEvent.VK_DIVIDE :
case KeyEvent.VK_BACK_QUOTE:
case KeyEvent.VK_QUOTE:
case KeyEvent.VK_DEAD_GRAVE:
@@ -202,28 +202,7 @@
//{{{ isNumericKeypad() method
public static boolean isNumericKeypad(int keyCode)
{
- switch(keyCode)
- {
- case KeyEvent.VK_NUMPAD0:
- case KeyEvent.VK_NUMPAD1:
- case KeyEvent.VK_NUMPAD2:
- case KeyEvent.VK_NUMPAD3:
- case KeyEvent.VK_NUMPAD4:
- case KeyEvent.VK_NUMPAD5:
- case KeyEvent.VK_NUMPAD6:
- case KeyEvent.VK_NUMPAD7:
- case KeyEvent.VK_NUMPAD8:
- case KeyEvent.VK_NUMPAD9:
- case KeyEvent.VK_MULTIPLY:
- case KeyEvent.VK_ADD:
- /* case KeyEvent.VK_SEPARATOR: */
- case KeyEvent.VK_SUBTRACT:
- case KeyEvent.VK_DECIMAL:
- case KeyEvent.VK_DIVIDE:
- return true;
- default:
- return false;
- }
+ return false;
} //}}}
//{{{ processKeyEvent() method