# HG changeset patch # User wenzelm # Date 1378285920 -7200 # Node ID b179cdfa9d82c8ba06eb39af9ebf21390641f377 # Parent 5e446969033c7120ba525fb3123e5c3790448d1c no completion on backspace -- too intrusive, e.g. when deleting keywords; diff -r 5e446969033c -r b179cdfa9d82 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Sep 04 10:46:57 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Wed Sep 04 11:12:00 2013 +0200 @@ -155,21 +155,21 @@ if (PIDE.options.bool("jedit_completion")) { if (!evt.isConsumed) { dismissed() + if (evt.getKeyChar != '\b') { + val mod = evt.getModifiers + val special = + // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java + (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 || + (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && + !Debug.ALT_KEY_PRESSED_DISABLED || + (mod & InputEvent.META_MASK) != 0 - val mod = evt.getModifiers - val special = - evt.getKeyChar == '\b' || - // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java - (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 || - (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && - !Debug.ALT_KEY_PRESSED_DISABLED || - (mod & InputEvent.META_MASK) != 0 - - if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { - input_delay.revoke() - action(immediate = PIDE.options.bool("jedit_completion_immediate")) + if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { + input_delay.revoke() + action(immediate = PIDE.options.bool("jedit_completion_immediate")) + } + else input_delay.invoke() } - else input_delay.invoke() } } }