# HG changeset patch
# User wenzelm
# Date 1377614732 -7200
# Node ID 423e29f1f304e0e326b5851f9958796b4337db16
# Parent  6589ff56cc3c64c65c3aec39f9ca8107ce805047
avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
uniform JEdit_Lib.propagate_key;

diff -r 6589ff56cc3c -r 423e29f1f304 src/Tools/jEdit/src/completion_popup.scala
--- 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()
   }
diff -r 6589ff56cc3c -r 423e29f1f304 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 27 16:09:28 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Aug 27 16:45:32 2013 +0200
@@ -108,21 +108,6 @@
   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
 
 
-  /* focus of main window */
-
-  def request_focus_view: Unit =
-  {
-    jEdit.getActiveView() match {
-      case null =>
-      case view =>
-        view.getTextArea match {
-          case null =>
-          case text_area => text_area.requestFocus
-        }
-    }
-  }
-
-
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
@@ -304,7 +289,22 @@
     }
 
 
-  /* key listener */
+  /* key event handling */
+
+  def request_focus_view
+  {
+    val view = jEdit.getActiveView()
+    if (view != null) {
+      val text_area = view.getTextArea
+      if (text_area != null) text_area.requestFocus
+    }
+  }
+
+  def propagate_key(view: View, evt: KeyEvent)
+  {
+    if (view != null && !evt.isConsumed)
+      view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
+  }
 
   def key_listener(
     workaround: Boolean = true,
diff -r 6589ff56cc3c -r 423e29f1f304 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Aug 27 16:09:28 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Aug 27 16:45:32 2013 +0200
@@ -181,13 +181,11 @@
 
           case _ =>
         }
-        if (propagate_keys && !evt.isConsumed)
-          view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
+        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
       },
     key_typed = (evt: KeyEvent) =>
       {
-        if (propagate_keys && !evt.isConsumed)
-          view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
+        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
       }
     )
   )