src/Tools/jEdit/src/completion_popup.scala
changeset 53296 65c60c782da5
parent 53293 fd27b8f5a479
child 53297 64c31de7f21c
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:08:02 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:35:50 2013 +0200
     1.3 @@ -10,13 +10,13 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.{Font, Point, BorderLayout, Dimension}
     1.7 -import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.8 +import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     1.9  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    1.10  
    1.11  import scala.swing.{ListView, ScrollPane}
    1.12  import scala.swing.event.MouseClicked
    1.13  
    1.14 -import org.gjt.sp.jedit.View
    1.15 +import org.gjt.sp.jedit.{View, Debug}
    1.16  import org.gjt.sp.jedit.textarea.JEditTextArea
    1.17  
    1.18  
    1.19 @@ -106,7 +106,7 @@
    1.20              val text = buffer.getSegment(start, caret - start)
    1.21  
    1.22              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    1.23 -              case Some((_, List(item))) if immediate =>
    1.24 +              case Some((_, List(item))) if item.immediate && immediate =>
    1.25                  insert(item)
    1.26  
    1.27                case Some((original, items)) =>
    1.28 @@ -148,7 +148,17 @@
    1.29        if (PIDE.options.bool("jedit_completion")) {
    1.30          if (!evt.isConsumed) {
    1.31            dismissed()
    1.32 -          if (PIDE.options.seconds("jedit_completion_delay").is_zero) {
    1.33 +
    1.34 +          val mod = evt.getModifiers
    1.35 +          val special =
    1.36 +            evt.getKeyChar == '\b' ||
    1.37 +            // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
    1.38 +            (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
    1.39 +            (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
    1.40 +              !Debug.ALT_KEY_PRESSED_DISABLED ||
    1.41 +            (mod & InputEvent.META_MASK) != 0
    1.42 +
    1.43 +          if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
    1.44              input_delay.revoke()
    1.45              action(PIDE.options.bool("jedit_completion_immediate"))
    1.46            }