less aggressive immediate completion, based on input and text;
authorwenzelm
Thu Aug 29 22:35:50 2013 +0200 (2013-08-29 ago)
changeset 5329665c60c782da5
parent 53295 45be26b98ca6
child 53297 64c31de7f21c
less aggressive immediate completion, based on input and text;
src/Pure/Isar/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/Isar/completion.scala	Thu Aug 29 22:08:02 2013 +0200
     1.2 +++ b/src/Pure/Isar/completion.scala	Thu Aug 29 22:35:50 2013 +0200
     1.3 @@ -13,7 +13,11 @@
     1.4  {
     1.5    /* items */
     1.6  
     1.7 -  sealed case class Item(original: String, replacement: String, description: String)
     1.8 +  sealed case class Item(
     1.9 +    original: String,
    1.10 +    replacement: String,
    1.11 +    description: String,
    1.12 +    immediate: Boolean)
    1.13    { override def toString: String = description }
    1.14  
    1.15  
    1.16 @@ -107,7 +111,10 @@
    1.17        case Some((word, cs)) =>
    1.18          val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
    1.19          if (ds.isEmpty) None
    1.20 -        else Some((word, ds.map(s => Completion.Item(word, s, s))))
    1.21 +        else {
    1.22 +          val immediate = !Completion.is_word(word)
    1.23 +          Some((word, ds.map(s => Completion.Item(word, s, s, immediate))))
    1.24 +        }
    1.25        case None => None
    1.26      }
    1.27    }
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:08:02 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:35:50 2013 +0200
     2.3 @@ -10,13 +10,13 @@
     2.4  import isabelle._
     2.5  
     2.6  import java.awt.{Font, Point, BorderLayout, Dimension}
     2.7 -import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     2.8 +import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
     2.9  import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    2.10  
    2.11  import scala.swing.{ListView, ScrollPane}
    2.12  import scala.swing.event.MouseClicked
    2.13  
    2.14 -import org.gjt.sp.jedit.View
    2.15 +import org.gjt.sp.jedit.{View, Debug}
    2.16  import org.gjt.sp.jedit.textarea.JEditTextArea
    2.17  
    2.18  
    2.19 @@ -106,7 +106,7 @@
    2.20              val text = buffer.getSegment(start, caret - start)
    2.21  
    2.22              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    2.23 -              case Some((_, List(item))) if immediate =>
    2.24 +              case Some((_, List(item))) if item.immediate && immediate =>
    2.25                  insert(item)
    2.26  
    2.27                case Some((original, items)) =>
    2.28 @@ -148,7 +148,17 @@
    2.29        if (PIDE.options.bool("jedit_completion")) {
    2.30          if (!evt.isConsumed) {
    2.31            dismissed()
    2.32 -          if (PIDE.options.seconds("jedit_completion_delay").is_zero) {
    2.33 +
    2.34 +          val mod = evt.getModifiers
    2.35 +          val special =
    2.36 +            evt.getKeyChar == '\b' ||
    2.37 +            // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
    2.38 +            (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
    2.39 +            (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
    2.40 +              !Debug.ALT_KEY_PRESSED_DISABLED ||
    2.41 +            (mod & InputEvent.META_MASK) != 0
    2.42 +
    2.43 +          if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
    2.44              input_delay.revoke()
    2.45              action(PIDE.options.bool("jedit_completion_immediate"))
    2.46            }