src/Tools/jEdit/src/completion_popup.scala
changeset 53231 423e29f1f304
parent 53230 6589ff56cc3c
child 53232 4a3762693452
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:09:28 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:45:32 2013 +0200
     1.3 @@ -155,27 +155,14 @@
     1.4                    hide_popup()
     1.5              }
     1.6            }
     1.7 -          if (!e.isConsumed) pass_to_view(e)
     1.8 +          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
     1.9          },
    1.10        key_typed = (e: KeyEvent) =>
    1.11          {
    1.12 -          if (!e.isConsumed) pass_to_view(e)
    1.13 +          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
    1.14          }
    1.15      )
    1.16  
    1.17 -  private def pass_to_view(e: KeyEvent)
    1.18 -  {
    1.19 -    opt_view match {
    1.20 -      case Some(view) if view.getKeyEventInterceptor == key_listener =>
    1.21 -        try {
    1.22 -          view.setKeyEventInterceptor(null)
    1.23 -          view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false)
    1.24 -        }
    1.25 -        finally { view.setKeyEventInterceptor(key_listener) }
    1.26 -      case _ =>
    1.27 -    }
    1.28 -  }
    1.29 -
    1.30    list_view.peer.addKeyListener(key_listener)
    1.31  
    1.32    list_view.peer.addMouseListener(new MouseAdapter {
    1.33 @@ -233,18 +220,12 @@
    1.34  
    1.35    def show_popup()
    1.36    {
    1.37 -    opt_view.foreach(view => view.setKeyEventInterceptor(key_listener))
    1.38      popup.show
    1.39      list_view.requestFocus
    1.40    }
    1.41  
    1.42    def hide_popup()
    1.43    {
    1.44 -    opt_view match {
    1.45 -      case Some(view) if (view.getKeyEventInterceptor == key_listener) =>
    1.46 -        view.setKeyEventInterceptor(null)
    1.47 -      case _ =>
    1.48 -    }
    1.49      popup.hide
    1.50      hidden()
    1.51    }