KeyEventWorkaround.java describes itself as "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." Most of
that has already been removed in the upgrade to Java 7, which is more uniform between
platforms than past Java versions, so extra tricks are normally not required.
The present reform is about NUMPAD keys -- keys produced with Numlock enabled. In
certain situations of using KeyEventWorkaround.processKeyEvent outside the normal
text area (e.g. in the Navigator plugin with its NavHistoryPopup, or a similar popup
in the Isabelle plugin), it is impossible to get NUMPAD keys, because that workaround
destroys them.
Almost two years ago, I have already removed that special case for Isabelle/jEdit
-- see http://isabelle.in.tum.de/repos/isabelle/rev/2a64cae5e611 which says "disable
some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava
Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads".
Many people have used that successfully on Linux, Windows, Mac OS X since September
2013.
The included patch removes that presumably obsolete workaround more thoroughly from
the jEdit code base, together with funny comments like "this is retarded. excuse me
while I drool and make stupid noises".
Submitted | makarius - 2015-08-25 18:51:49.833000 | Assigned | |
---|---|---|---|
Priority | 5 | Labels | |
Status | open | Group | None |
Resolution | None |
2015-08-25 18:55:46.755000 makarius |
See also https://sourceforge.net/p/jedit/plugin-patches/176 for a patch that is required to make Navigator actually work, with key strokes in its popup. The extended patch below shows how it could handle NUMPAD digits, in addition to ordinary digits. Without the keyeventworkaround.patch it could not do that: NUMPAD keys would get destroyed. navigator.patch (1.5Kio) |
---|---|
2015-08-25 19:00:41.127000 makarius |
A more ambitious reform in that corner could probably do away with the special ALT key handling on Windows, too. At least the quoted issue http://bugs.sun.com/view_bug.do?bug_id=6458497 from KeyEventWorkaround.java seems to be closed. Since I am not as fluent on Windows as on the other platforms, I did not explore this further. |
2015-08-30 15:52:34.589000 ezust |
Can you please describe steps to reproduce any bugs your patch might fix, so I can
test the before/after effect of your patch with my own build on Linux?
|
2015-08-30 21:15:58.513000 makarius |
See the navigator.patch above, and the reference to plugin-patches/176. After putting
the Navigator into shape, it is possible to see the difference: before it cannot handle
NUMPAD keys, after it can handle them. (Without the Navigator patch, it just crashes.)
|