added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);

--- a/src/Tools/jEdit/etc/options	Fri Nov 08 15:10:16 2013 +0100
+++ b/src/Tools/jEdit/etc/options	Fri Nov 08 17:34:37 2013 +0100
@@ -42,6 +42,9 @@
 public option jedit_completion_delay : real = 0.0
   -- "delay for completion popup (seconds)"
 
+public option jedit_completion_dismiss_delay : real = 0.0
+  -- "delay for dismissing obsolete completion popup (seconds)"
+
 public option jedit_completion_immediate : bool = false
   -- "insert unique completion immediately into buffer (if delay = 0)"
 

--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 15:10:16 2013 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 17:34:37 2013 +0100
@@ -488,10 +488,18 @@
     list_view.requestFocus
   }
 
+  private val hide_popup_delay =
+    Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
+      popup.hide
+    }
+
   private def hide_popup()
   {
     if (list_view.peer.isFocusOwner) refocus()
-    popup.hide
+
+    if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero)
+      popup.hide
+    else hide_popup_delay.invoke()
   }
 }