src/Tools/jEdit/src/completion_popup.scala
changeset 53397 b179cdfa9d82
parent 53337 b3817a0e3211
child 53398 f8b150e8778b
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Sep 04 10:46:57 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Sep 04 11:12:00 2013 +0200
     1.3 @@ -155,21 +155,21 @@
     1.4        if (PIDE.options.bool("jedit_completion")) {
     1.5          if (!evt.isConsumed) {
     1.6            dismissed()
     1.7 +          if (evt.getKeyChar != '\b') {
     1.8 +            val mod = evt.getModifiers
     1.9 +            val special =
    1.10 +              // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
    1.11 +              (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
    1.12 +              (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
    1.13 +                !Debug.ALT_KEY_PRESSED_DISABLED ||
    1.14 +              (mod & InputEvent.META_MASK) != 0
    1.15  
    1.16 -          val mod = evt.getModifiers
    1.17 -          val special =
    1.18 -            evt.getKeyChar == '\b' ||
    1.19 -            // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
    1.20 -            (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
    1.21 -            (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
    1.22 -              !Debug.ALT_KEY_PRESSED_DISABLED ||
    1.23 -            (mod & InputEvent.META_MASK) != 0
    1.24 -
    1.25 -          if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
    1.26 -            input_delay.revoke()
    1.27 -            action(immediate = PIDE.options.bool("jedit_completion_immediate"))
    1.28 +            if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
    1.29 +              input_delay.revoke()
    1.30 +              action(immediate = PIDE.options.bool("jedit_completion_immediate"))
    1.31 +            }
    1.32 +            else input_delay.invoke()
    1.33            }
    1.34 -          else input_delay.invoke()
    1.35          }
    1.36        }
    1.37      }