On Fri, 30 Aug 2013, Makarius wrote:
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.)
I have made some quick tests with my Sony Vaio at home, with its slightly
odd arrangement of cursor keys and numeric keypad. The *numeric* mode of
it is indeed dead -- I am normally using it for cursor movement, in order
to be able to use that keyboard at all.
This needs more investigation, but is probably due to the activation of
some worarounds of jEdit that are explained in its sources like this:
/** Various hacks to get keyboard event handling to behave in a consistent
manner
* across Java implementations. This type of stuff should not be necessary, but
* Java's keyboard handling is crap, to put it mildly.
*
* @author Slava Pestov
*/
It was probably a mistake to heed comments in code -- they are usually
very unreliably source of information.
What did improve, though, was a situation with ESCAPE handling when
tooltips compete with text selection.
Anyway, it looks like another dive into the depths of history of keyboard
handling on Windows, Linux, Mac OS X -- the JVM has preserved all the old
ways faithfully.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
