On 08/30/2013 02:21 PM, Makarius wrote:
On Thu, 29 Aug 2013, Ondřej Kunčar wrote:
This refers to 3c26a7042d8e. The numpad stopped working in JEdit.
Reproducible on my machine and also on Dmitriy's machine. We use Linux.
What exactly means stopped working? Can you give another changeset where
it still works, whatever that means here?
Note that I have recently changed many Isabelle/jEdit keyboard
shortcuts. This might cause some confusion with the persistent
$ISABELLE_HOME_USER/jedit/keymaps/ -- deleting that directory makes a
fresh start (and looses personal keybindings, if you have any).
Makarius
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. Usually the same
symbol that is on the key. This is the only feature of the numpad that I
know. And this is the feature that is broken: if I press a key from the
numpad, I don't get any symbol on my display in the main editing area in
JEdit.
It doesn't work for me, Dmitriy, Jasmin, Tobias and Lars. That already
means a couple of different systems: Linux (different distribution), Mac OS.
Removing $ISABELLE_HOME_USER/jedit/keymaps/ didn't help.
It still doesn't work in c31c0c311cf0.
It works for example in ca237b9e4542.
Just a personal question: did you try to use the numpad on your keyboard
before you sent your reply?
Ondrej
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
