Some further refinements here:
changeset: 53398:f8b150e8778b
user: wenzelm
date: Wed Sep 04 12:20:00 2013 +0200
files: NEWS src/Tools/jEdit/src/completion_popup.scala
description:
remove Swing input map, which might bind keys in unexpected ways (e.g.
LEFT/RIGHT in singleton list);
handle KP_UP/KP_DOWN keys as well, like Swing does;
There was somehow strange behaviour, especially with singleton JList
popups interpreting cursor LEFT / RIGHT keys in unknown ways, and thus
preventing the jEdit text area to do so for plain cursor movement.
People with a numpad that has a numlock modifier can try if KP_UP/KP_DOWN
actually works.
I do not really understand Swing InputMap of JComponent. Resetting all
that to null seems to avoid Swing or any user-defined LAF interfering, but
it might have other consequences to make such a hard reset on system
defaults.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
