author | wenzelm |
Mon, 17 Mar 2014 14:40:59 +0100 | |
changeset 56177 | bfa9dfb722de |
parent 56176 | 0bc9b0ad6287 |
child 56178 | 2a6f58938573 |
child 56184 | a2bd40830593 |
--- 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 }