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