# HG changeset patch
# User wenzelm
# Date 1377808550 -7200
# Node ID 65c60c782da564e927bb99d477f48a31a83c9105
# Parent  45be26b98ca6e9feb135a1bf4e4c48d76ea065af
less aggressive immediate completion, based on input and text;

diff -r 45be26b98ca6 -r 65c60c782da5 src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Thu Aug 29 22:08:02 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Thu Aug 29 22:35:50 2013 +0200
@@ -13,7 +13,11 @@
 {
   /* items */
 
-  sealed case class Item(original: String, replacement: String, description: String)
+  sealed case class Item(
+    original: String,
+    replacement: String,
+    description: String,
+    immediate: Boolean)
   { override def toString: String = description }
 
 
@@ -107,7 +111,10 @@
       case Some((word, cs)) =>
         val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
         if (ds.isEmpty) None
-        else Some((word, ds.map(s => Completion.Item(word, s, s))))
+        else {
+          val immediate = !Completion.is_word(word)
+          Some((word, ds.map(s => Completion.Item(word, s, s, immediate))))
+        }
       case None => None
     }
   }
diff -r 45be26b98ca6 -r 65c60c782da5 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:08:02 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:35:50 2013 +0200
@@ -10,13 +10,13 @@
 import isabelle._
 
 import java.awt.{Font, Point, BorderLayout, Dimension}
-import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
+import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
 import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
 
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{View, Debug}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
@@ -106,7 +106,7 @@
             val text = buffer.getSegment(start, caret - start)
 
             syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
-              case Some((_, List(item))) if immediate =>
+              case Some((_, List(item))) if item.immediate && immediate =>
                 insert(item)
 
               case Some((original, items)) =>
@@ -148,7 +148,17 @@
       if (PIDE.options.bool("jedit_completion")) {
         if (!evt.isConsumed) {
           dismissed()
-          if (PIDE.options.seconds("jedit_completion_delay").is_zero) {
+
+          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(PIDE.options.bool("jedit_completion_immediate"))
           }