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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
