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 }