src/Tools/jEdit/src/completion_popup.scala
changeset 56177 bfa9dfb722de
parent 56175 79c29244b377
child 56197 416f7a00e4cb
equal deleted inserted replaced
56176:0bc9b0ad6287 56177:bfa9dfb722de
    64 
    64 
    65     def action(text_area: TextArea): Boolean =
    65     def action(text_area: TextArea): Boolean =
    66       apply(text_area) match {
    66       apply(text_area) match {
    67         case Some(text_area_completion) =>
    67         case Some(text_area_completion) =>
    68           if (text_area_completion.active_range.isDefined)
    68           if (text_area_completion.active_range.isDefined)
       
    69             text_area_completion.action()
       
    70           else
    69             text_area_completion.action(immediate = true, explicit = true)
    71             text_area_completion.action(immediate = true, explicit = true)
    70           else text_area_completion.action()
       
    71           true
    72           true
    72         case None => false
    73         case None => false
    73       }
    74       }
    74 
    75 
    75     def exit(text_area: JEditTextArea)
    76     def exit(text_area: JEditTextArea)