[isabelle-dev] NEWS: Improved completion mechanism

[Makarius]

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