# HG changeset patch
# User wenzelm
# Date 1308513184 -7200
# Node ID 265d9300d523cb5bccbf26bedb096244e97a06d0
# Parent  0a2ffb071fcaeaf9c158ff867c3c8f56bdca40ce
treat quotes as non-controllable, to reduce surprise in incremental editing;

diff -r 0a2ffb071fca -r 265d9300d523 src/Tools/jEdit/src/token_markup.scala
--- 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)
           }