# HG changeset patch
# User wenzelm
# Date 1399140649 -7200
# Node ID 879fe16bd27c06d9e7f0528f2b19f4a85889043e
# Parent  94477e9ff063c6aa33148d4b170ecda05f248fcf
propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);

diff -r 94477e9ff063 -r 879fe16bd27c 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)