src/Tools/jEdit/src/completion_popup.scala
changeset 53231 423e29f1f304
parent 53230 6589ff56cc3c
child 53232 4a3762693452
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:09:28 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:45:32 2013 +0200
@@ -155,27 +155,14 @@
                   hide_popup()
             }
           }
-          if (!e.isConsumed) pass_to_view(e)
+          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
         },
       key_typed = (e: KeyEvent) =>
         {
-          if (!e.isConsumed) pass_to_view(e)
+          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
         }
     )
 
-  private def pass_to_view(e: KeyEvent)
-  {
-    opt_view match {
-      case Some(view) if view.getKeyEventInterceptor == key_listener =>
-        try {
-          view.setKeyEventInterceptor(null)
-          view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false)
-        }
-        finally { view.setKeyEventInterceptor(key_listener) }
-      case _ =>
-    }
-  }
-
   list_view.peer.addKeyListener(key_listener)
 
   list_view.peer.addMouseListener(new MouseAdapter {
@@ -233,18 +220,12 @@
 
   def show_popup()
   {
-    opt_view.foreach(view => view.setKeyEventInterceptor(key_listener))
     popup.show
     list_view.requestFocus
   }
 
   def hide_popup()
   {
-    opt_view match {
-      case Some(view) if (view.getKeyEventInterceptor == key_listener) =>
-        view.setKeyEventInterceptor(null)
-      case _ =>
-    }
     popup.hide
     hidden()
   }