# HG changeset patch
# User wenzelm
# Date 1383928477 -3600
# Node ID 75056198682839c353e95f84d9752be7e99926d6
# Parent  3eb84b6b0353a8604c2c276e35462ba09a1f46e8
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);

diff -r 3eb84b6b0353 -r 750561986828 src/Tools/jEdit/etc/options
--- 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)"
 
diff -r 3eb84b6b0353 -r 750561986828 src/Tools/jEdit/src/completion_popup.scala
--- 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()
   }
 }