--- 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
