immediate completion even with delay, which is the default according to 638b29331549;
authorwenzelm
Sun, 30 Mar 2014 21:03:40 +0200
changeset 56326 c3d7b3bb2708
parent 56325 ffbfc92e6508
child 56327 3e62e68fb342
immediate completion even with delay, which is the default according to 638b29331549;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/etc/options	Sun Mar 30 20:23:26 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Sun Mar 30 21:03:40 2014 +0200
@@ -46,7 +46,7 @@
   -- "delay for completion popup (seconds)"
 
 public option jedit_completion_immediate : bool = false
-  -- "insert unique completion immediately into buffer (if delay = 0)"
+  -- "insert uniquely completed abbreviation immediately into buffer"
 
 
 section "Rendering of Document Content"
--- a/src/Tools/jEdit/src/completion_popup.scala	Sun Mar 30 20:23:26 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Mar 30 21:03:40 2014 +0200
@@ -231,7 +231,8 @@
       }
     }
 
-    def action(immediate: Boolean = false, explicit: Boolean = false)
+    def action(immediate: Boolean = false, explicit: Boolean = false, delayed: Boolean = false)
+      : Boolean =
     {
       val view = text_area.getView
       val layered = view.getLayeredPane
@@ -315,7 +316,8 @@
               (false, None, None)
           }
         }
-        if (!no_completion) {
+        if (no_completion) false
+        else {
           val result =
             Completion.Result.merge(history,
               semantic_completion, syntax_completion(history, explicit, opt_rendering))
@@ -325,14 +327,17 @@
               result.items match {
                 case List(item) if result.unique && item.immediate && immediate =>
                   insert(item)
-                case _ :: _ =>
+                  true
+                case _ :: _ if !delayed =>
                   open_popup(result)
-                case _ =>
+                  false
+                case _ => false
               }
-            case None =>
+            case None => false
           }
         }
       }
+      else false
     }
 
 
@@ -347,11 +352,17 @@
           dismissed()
           if (evt.getKeyChar != '\b') {
             val special = JEdit_Lib.special_key(evt)
+            val immediate = PIDE.options.bool("jedit_completion_immediate")
             if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
               input_delay.revoke()
-              action(immediate = PIDE.options.bool("jedit_completion_immediate"))
+              action(immediate = immediate)
             }
-            else input_delay.invoke()
+            else {
+              if (!special && action(immediate = immediate, delayed = true))
+                input_delay.revoke()
+              else
+                input_delay.invoke()
+            }
           }
         }
       }