src/Tools/jEdit/src/token_markup.scala

     {
       for (i <- start until stop) result += (i -> style)
     }
     var offset = 0
     var ctrl = ""
-    for (sym <- Symbol.iterator(text).map(_.toString)) {
+    for (sym <- Symbol.iterator_string(text)) {
       if (ctrl_style(sym).isDefined) ctrl = sym
       else if (ctrl != "") {
         if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
           mark(offset - ctrl.length, offset, _ => hidden)
           mark(offset, offset + sym.length, ctrl_style(ctrl).get)