propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
authorwenzelm
Sat, 03 May 2014 20:10:49 +0200
changeset 56840 879fe16bd27c
parent 56839 94477e9ff063
child 56841 bc6faeadbf82
propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
src/Tools/jEdit/src/completion_popup.scala
--- 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)