# HG changeset patch
# User wenzelm
# Date 1395052389 -3600
# Node ID 15351577da10396a839a85f95dad614e4ba5e4b2
# Parent  638b293315491ec54a3aa5ecfdaf3946dd4079ad
clarified key event propagation, in accordance to outer_key_listener;

diff -r 638b29331549 -r 15351577da10 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 10:45:29 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 11:33:09 2014 +0100
@@ -246,7 +246,7 @@
               }
               override def propagate(evt: KeyEvent) {
                 JEdit_Lib.propagate_key(view, evt)
-                input(evt)
+                if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
               }
               override def refocus() { text_area.requestFocus }
             }