propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
authorwenzelm
Sat May 03 20:10:49 2014 +0200 (2014-05-03 ago)
changeset 56840879fe16bd27c
parent 56839 94477e9ff063
child 56841 bc6faeadbf82
propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri May 02 23:31:25 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat May 03 20:10:49 2014 +0200
     1.3 @@ -270,7 +270,9 @@
     1.4                  insert(item)
     1.5                }
     1.6                override def propagate(evt: KeyEvent) {
     1.7 -                if (view.getKeyEventInterceptor == inner_key_listener) {
     1.8 +                if (view.getKeyEventInterceptor == null)
     1.9 +                  JEdit_Lib.propagate_key(view, evt)
    1.10 +                else if (view.getKeyEventInterceptor == inner_key_listener) {
    1.11                    try {
    1.12                      view.setKeyEventInterceptor(null)
    1.13                      JEdit_Lib.propagate_key(view, evt)