added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
authorwenzelm
Fri Nov 08 17:34:37 2013 +0100 (2013-11-08 ago)
changeset 54377750561986828
parent 54376 3eb84b6b0353
child 54378 72254819befd
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Fri Nov 08 15:10:16 2013 +0100
     1.2 +++ b/src/Tools/jEdit/etc/options	Fri Nov 08 17:34:37 2013 +0100
     1.3 @@ -42,6 +42,9 @@
     1.4  public option jedit_completion_delay : real = 0.0
     1.5    -- "delay for completion popup (seconds)"
     1.6  
     1.7 +public option jedit_completion_dismiss_delay : real = 0.0
     1.8 +  -- "delay for dismissing obsolete completion popup (seconds)"
     1.9 +
    1.10  public option jedit_completion_immediate : bool = false
    1.11    -- "insert unique completion immediately into buffer (if delay = 0)"
    1.12  
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 15:10:16 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Nov 08 17:34:37 2013 +0100
     2.3 @@ -488,10 +488,18 @@
     2.4      list_view.requestFocus
     2.5    }
     2.6  
     2.7 +  private val hide_popup_delay =
     2.8 +    Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
     2.9 +      popup.hide
    2.10 +    }
    2.11 +
    2.12    private def hide_popup()
    2.13    {
    2.14      if (list_view.peer.isFocusOwner) refocus()
    2.15 -    popup.hide
    2.16 +
    2.17 +    if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero)
    2.18 +      popup.hide
    2.19 +    else hide_popup_delay.invoke()
    2.20    }
    2.21  }
    2.22