1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Jan 01 11:36:30 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jan 01 13:37:37 2013 +0100
     1.3 @@ -47,6 +47,15 @@
     1.4  
     1.5      val buffer = text_area.getBuffer
     1.6  
     1.7 +    text_area.getSelection.foreach(sel => {
     1.8 +      val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
     1.9 +      JEdit_Lib.try_get_text(buffer, before) match {
    1.10 +        case Some(s) if is_control_style(s) =>
    1.11 +          text_area.extendSelection(before.start, before.stop)
    1.12 +        case _ =>
    1.13 +      }
    1.14 +    })
    1.15 +
    1.16      text_area.getSelection.toList match {
    1.17        case Nil =>
    1.18          text_area.setSelectedText(control)