propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
--- a/src/Tools/jEdit/src/completion_popup.scala Fri May 02 23:31:25 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat May 03 20:10:49 2014 +0200
@@ -270,7 +270,9 @@
insert(item)
}
override def propagate(evt: KeyEvent) {
- if (view.getKeyEventInterceptor == inner_key_listener) {
+ if (view.getKeyEventInterceptor == null)
+ JEdit_Lib.propagate_key(view, evt)
+ else if (view.getKeyEventInterceptor == inner_key_listener) {
try {
view.setKeyEventInterceptor(null)
JEdit_Lib.propagate_key(view, evt)