proper flags for main action (amending 638b29331549);
authorwenzelm
Mon Mar 17 14:40:59 2014 +0100 (2014-03-17)
changeset 56177bfa9dfb722de
parent 56176 0bc9b0ad6287
child 56178 2a6f58938573
child 56184 a2bd40830593
proper flags for main action (amending 638b29331549);
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 14:37:23 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 14:40:59 2014 +0100
     1.3 @@ -66,8 +66,9 @@
     1.4        apply(text_area) match {
     1.5          case Some(text_area_completion) =>
     1.6            if (text_area_completion.active_range.isDefined)
     1.7 +            text_area_completion.action()
     1.8 +          else
     1.9              text_area_completion.action(immediate = true, explicit = true)
    1.10 -          else text_area_completion.action()
    1.11            true
    1.12          case None => false
    1.13        }