treat quotes as non-controllable, to reduce surprise in incremental editing;

--- a/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 21:47:14 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Jun 19 21:53:04 2011 +0200
@@ -49,7 +49,7 @@
       for (sym <- Symbol.iterator(text).map(_.toString)) {
         if (ctrl_style(sym).isDefined) ctrl = sym
         else if (ctrl != "") {
-          if (symbols.is_controllable(sym)) {
+          if (symbols.is_controllable(sym) && sym != "\"") {
             mark(offset - ctrl.length, offset, _ => hidden)
             mark(offset, offset + sym.length, ctrl_style(ctrl).get)
           }