[isabelle-dev] numpad doesn't work

[Makarius]

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