src/Tools/jEdit/src/completion_popup.scala
changeset 56177 bfa9dfb722de
parent 56175 79c29244b377
child 56197 416f7a00e4cb
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 14:37:23 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 14:40:59 2014 +0100
@@ -66,8 +66,9 @@
       apply(text_area) match {
         case Some(text_area_completion) =>
           if (text_area_completion.active_range.isDefined)
+            text_area_completion.action()
+          else
             text_area_completion.action(immediate = true, explicit = true)
-          else text_area_completion.action()
           true
         case None => false
       }