--- a/src/Tools/jEdit/src/token_markup.scala Tue Jan 01 11:36:30 2013 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Jan 01 13:37:37 2013 +0100
@@ -47,6 +47,15 @@
val buffer = text_area.getBuffer
+ text_area.getSelection.foreach(sel => {
+ val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
+ JEdit_Lib.try_get_text(buffer, before) match {
+ case Some(s) if is_control_style(s) =>
+ text_area.extendSelection(before.start, before.stop)
+ case _ =>
+ }
+ })
+
text_area.getSelection.toList match {
case Nil =>
text_area.setSelectedText(control)