# HG changeset patch
# User wenzelm
# Date 1395049529 -3600
# Node ID 638b293315491ec54a3aa5ecfdaf3946dd4079ad
# Parent  9b0dc5c704c91dc8f0fec437c426dbdb9e3d9e32
allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
clarified isabelle.completion action: already open popup is re-opened and thus updated;

diff -r 9b0dc5c704c9 -r 638b29331549 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Mar 17 10:11:23 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Mar 17 10:45:29 2014 +0100
@@ -42,7 +42,7 @@
 public option jedit_completion : bool = true
   -- "enable completion popup"
 
-public option jedit_completion_delay : real = 0.0
+public option jedit_completion_delay : real = 0.5
   -- "delay for completion popup (seconds)"
 
 public option jedit_completion_dismiss_delay : real = 0.0
diff -r 9b0dc5c704c9 -r 638b29331549 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 10:11:23 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 10:45:29 2014 +0100
@@ -62,6 +62,16 @@
         case None => None
       }
 
+    def action(text_area: TextArea): Boolean =
+      apply(text_area) match {
+        case Some(text_area_completion) =>
+          if (text_area_completion.active_range.isDefined)
+            text_area_completion.action(immediate = true, explicit = true)
+          else text_area_completion.action()
+          true
+        case None => false
+      }
+
     def exit(text_area: JEditTextArea)
     {
       Swing_Thread.require()
@@ -180,7 +190,7 @@
     }
 
 
-    /* completion action */
+    /* completion action: text area */
 
     private def insert(item: Completion.Item)
     {
@@ -247,25 +257,22 @@
       }
 
       def semantic_completion(): Option[Completion.Result] =
-        if (explicit) {
-          PIDE.document_view(text_area) match {
-            case Some(doc_view) =>
-              val rendering = doc_view.get_rendering()
-              rendering.completion_names(before_caret_range(rendering)) match {
-                case Some(names) =>
-                  if (names.no_completion)
-                    Some(Completion.Result.empty(names.range))
-                  else
-                    JEdit_Lib.try_get_text(buffer, names.range) match {
-                      case Some(original) => names.complete(history, decode, original)
-                      case None => None
-                    }
-                case None => None
-              }
-            case None => None
-          }
+        PIDE.document_view(text_area) match {
+          case Some(doc_view) =>
+            val rendering = doc_view.get_rendering()
+            rendering.completion_names(before_caret_range(rendering)) match {
+              case Some(names) =>
+                if (names.no_completion)
+                  Some(Completion.Result.empty(names.range))
+                else
+                  JEdit_Lib.try_get_text(buffer, names.range) match {
+                    case Some(original) => names.complete(history, decode, original)
+                    case None => None
+                  }
+              case None => None
+            }
+          case None => None
         }
-        else None
 
       if (buffer.isEditable) {
         semantic_completion() orElse syntax_completion(explicit) match {
@@ -401,7 +408,7 @@
     }
 
 
-    /* completion action */
+    /* completion action: text field */
 
     def action()
     {
diff -r 9b0dc5c704c9 -r 638b29331549 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Mar 17 10:11:23 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Mar 17 10:45:29 2014 +0100
@@ -247,11 +247,8 @@
 
   def complete(view: View)
   {
-    Completion_Popup.Text_Area(view.getTextArea) match {
-      case Some(text_area_completion) =>
-        text_area_completion.action(immediate = true, explicit = true)
-      case None => CompleteWord.completeWord(view)
-    }
+    if (!Completion_Popup.Text_Area.action(view.getTextArea))
+      CompleteWord.completeWord(view)
   }