On Tue, 10 Sep 2013, Makarius wrote:
In the meantime I have tried a few keyboards that still have a numpad --
they usually work with page or arrow movement, but not digits.
It needs further investigation to understand which of the "fixes" of
jEdit key handling needs to be avoided.
I've now made some investigations of jEdit history, using what looks like
a semi-official git mirror of its SVN:
http://jedit.git.sourceforge.net/git/gitweb.cgi?p=jedit/jEdit.bak;a=summary
It seems that in the past Slava Pestov has made many workarounds of the
key event model of various Java versions on different platforms, notably
in jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java. He was using both
very colorful language ("this is retarted", "this is crap"), and some
meaningless changelog entries like "foo" or "fixed bug". The last relevant
change was by Matthieu Casanova (08-Dec-2007).
In Isabelle/2a64cae5e611 I have now disabled any special treatment of the
numeric keypad, hoping for the best. (We are in a slightly better
situation, since Java 7 as bad as it might be is better than any earlier
versions of Java, and we have just this one version that is bundled with
Isabelle.)
I had also tried to avoid KeyEventWorkaround.processKeyEvent in
isabelle.jedit.JEdit_Lib.key_listener altogether, but then the completion
popup has problems competing for key events with the text area.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
