more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;

--- 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)