[isabelle-dev] numpad doesn't work

[Makarius]

On Fri, 30 Aug 2013, Ondřej Kunčar wrote:

> What do I exactly mean? Let me tell you what the numpad is. It is a part 
> of a keyboard and it has various keys. If you press one of the keys, you 
> get a corresponding symbol in an input on your display.

A numpad is far more complex than that.  It has various modifiers, and 
generally odd meaning of keys, with or without these modifiers.

I have been through long struggles with key events on various systems, 
keyboards etc.  Nothing what you think it is is actually there at the 
bottom.  Key handling has become a big challange on modern computers. 
This is no joke at all.


> Just a personal question: did you try to use the numpad on your keyboard 
> before you sent your reply?

No.

These days a numpad is relatively rare on keyboards.  (I have one at the 
big laptop at home, but it has quite different behaviour than the more 
regular numpads on old-style stand-alone keyboards.)


 	Makarius