src/Tools/jEdit/src/completion_popup.scala
changeset 54377 750561986828
parent 54376 3eb84b6b0353
child 55615 bf4bbe72f740
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 15:10:16 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 17:34:37 2013 +0100
     1.3 @@ -488,10 +488,18 @@
     1.4      list_view.requestFocus
     1.5    }
     1.6  
     1.7 +  private val hide_popup_delay =
     1.8 +    Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
     1.9 +      popup.hide
    1.10 +    }
    1.11 +
    1.12    private def hide_popup()
    1.13    {
    1.14      if (list_view.peer.isFocusOwner) refocus()
    1.15 -    popup.hide
    1.16 +
    1.17 +    if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero)
    1.18 +      popup.hide
    1.19 +    else hide_popup_delay.invoke()
    1.20    }
    1.21  }
    1.22