[isabelle-dev] numpad doesn't work

[Ondřej Kunčar]

On 09/02/2013 12:21 PM, Makarius wrote:
> 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.

The numeric mode is dead. The cursor mode is also partly dead. Home, 
PgUp, PgDn, End, Insert and Delete work but ArrowUp, ArrowDown, 
ArrowLeft and ArrowRight don't work either. Enter works in both modes.

And funnily enough, in the numeric mode, if I press any key (except for 
Enter) and there is a completion possible at the place where the cursor 
is, the completion dialog is shown.

Ondrej