diff -r 29af7bb89757 -r 2a64cae5e611 src/Tools/jEdit/patches/jedit/numeric_keypad
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/numeric_keypad	Tue Sep 10 22:37:01 2013 +0200
@@ -0,0 +1,50 @@
+--- 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