option to insert unique completion immediately into buffer;

--- a/src/Pure/General/time.scala	Thu Aug 29 20:46:55 2013 +0200
+++ b/src/Pure/General/time.scala	Thu Aug 29 21:17:46 2013 +0200
@@ -30,6 +30,7 @@
   def min(t: Time): Time = if (ms < t.ms) this else t
   def max(t: Time): Time = if (ms > t.ms) this else t
 
+  def is_zero: Boolean = ms == 0
   def is_relevant: Boolean = ms >= 1
 
   override def hashCode: Int = ms.hashCode

--- a/src/Tools/jEdit/etc/options	Thu Aug 29 20:46:55 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Aug 29 21:17:46 2013 +0200
@@ -39,6 +39,9 @@
 public option jedit_completion_delay : real = 0.0
   -- "delay for completion popup (seconds)"
 
+public option jedit_completion_immediate : bool = false
+  -- "insert unique completion immediately into buffer (if delay = 0)"
+
 
 section "Rendering of Document Content"
 

--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 20:46:55 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 21:17:46 2013 +0200
@@ -66,26 +66,10 @@
 
   class Text_Area private(text_area: JEditTextArea)
   {
-    /* popup state */
-
     private var completion_popup: Option[Completion_Popup] = None
 
-    def dismissed(): Boolean =
-    {
-      Swing_Thread.require()
 
-      completion_popup match {
-        case Some(completion) =>
-          completion.hide_popup()
-          completion_popup = None
-          true
-        case None =>
-          false
-      }
-    }
-
-
-    /* insert selected item */
+    /* completion action */
 
     private def insert(item: Completion.Item)
     {
@@ -106,8 +90,56 @@
       }
     }
 
+    def action(immediate: Boolean)
+    {
+      val view = text_area.getView
+      val layered = view.getLayeredPane
+      val buffer = text_area.getBuffer
+      val painter = text_area.getPainter
 
-    /* input of key events */
+      if (buffer.isEditable) {
+        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
+          case Some(syntax) =>
+            val caret = text_area.getCaretPosition
+            val line = buffer.getLineOfOffset(caret)
+            val start = buffer.getLineStartOffset(line)
+            val text = buffer.getSegment(start, caret - start)
+
+            syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
+              case Some((_, List(item))) if immediate =>
+                insert(item)
+
+              case Some((original, items)) =>
+                val font =
+                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+
+                val loc1 = text_area.offsetToXY(caret - original.length)
+                if (loc1 != null) {
+                  val loc2 =
+                    SwingUtilities.convertPoint(painter,
+                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+
+                  val completion =
+                    new Completion_Popup(layered, loc2, font, items) {
+                      override def complete(item: Completion.Item) { insert(item) }
+                      override def propagate(evt: KeyEvent) {
+                        JEdit_Lib.propagate_key(view, evt)
+                        input(evt)
+                      }
+                      override def refocus() { text_area.requestFocus }
+                    }
+                  completion_popup = Some(completion)
+                  completion.show_popup()
+                }
+              case None =>
+            }
+          case None =>
+        }
+      }
+    }
+
+
+    /* input key events */
 
     def input(evt: KeyEvent)
     {
@@ -116,7 +148,11 @@
       if (PIDE.options.bool("jedit_completion")) {
         if (!evt.isConsumed) {
           dismissed()
-          input_delay.invoke()
+          if (PIDE.options.seconds("jedit_completion_delay").is_zero) {
+            input_delay.revoke()
+            action(PIDE.options.bool("jedit_completion_immediate"))
+          }
+          else input_delay.invoke()
         }
       }
       else {
@@ -126,50 +162,26 @@
     }
 
     private val input_delay =
-      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
-      {
-        val view = text_area.getView
-        val layered = view.getLayeredPane
-        val buffer = text_area.getBuffer
-        val painter = text_area.getPainter
+      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+        action(false)
+      }
 
-        if (buffer.isEditable) {
-          Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
-            case Some(syntax) =>
-              val caret = text_area.getCaretPosition
-              val line = buffer.getLineOfOffset(caret)
-              val start = buffer.getLineStartOffset(line)
-              val text = buffer.getSegment(start, caret - start)
 
-              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
-                case Some((original, items)) =>
-                  val font =
-                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+    /* dismiss popup */
 
-                  val loc1 = text_area.offsetToXY(caret - original.length)
-                  if (loc1 != null) {
-                    val loc2 =
-                      SwingUtilities.convertPoint(painter,
-                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+    def dismissed(): Boolean =
+    {
+      Swing_Thread.require()
 
-                    val completion =
-                      new Completion_Popup(layered, loc2, font, items) {
-                        override def complete(item: Completion.Item) { insert(item) }
-                        override def propagate(evt: KeyEvent) {
-                          JEdit_Lib.propagate_key(view, evt)
-                          input(evt)
-                        }
-                        override def refocus() { text_area.requestFocus }
-                      }
-                    completion_popup = Some(completion)
-                    completion.show_popup()
-                  }
-                case None =>
-              }
-            case None =>
-          }
-        }
+      completion_popup match {
+        case Some(completion) =>
+          completion.hide_popup()
+          completion_popup = None
+          true
+        case None =>
+          false
       }
+    }
 
 
     /* activation */