src/Tools/jEdit/src/completion_popup.scala
changeset 56840 879fe16bd27c
parent 56662 f373fb77e0a4
child 56841 bc6faeadbf82
--- 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)