--- 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()
}
}