1.1 --- a/src/Pure/General/symbol.scala	Tue Jul 05 22:43:18 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Jul 05 23:18:14 2011 +0200
     1.3 @@ -64,11 +64,11 @@
     1.4  
     1.5    def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
     1.6  
     1.7 -  def is_physical_newline(s: CharSequence): Boolean =
     1.8 -    "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
     1.9 +  def is_physical_newline(s: String): Boolean =
    1.10 +    s == "\n" || s == "\r" || s == "\r\n"
    1.11  
    1.12 -  def is_malformed(s: CharSequence): Boolean =
    1.13 -    !(s.length == 1 && is_plain(s.charAt(0))) && malformed_symbol.pattern.matcher(s).matches
    1.14 +  def is_malformed(s: String): Boolean =
    1.15 +    !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
    1.16  
    1.17    class Matcher(text: CharSequence)
    1.18    {
    1.19 @@ -87,8 +87,11 @@
    1.20  
    1.21    /* efficient iterators */
    1.22  
    1.23 -  def iterator(text: CharSequence): Iterator[CharSequence] =
    1.24 -    new Iterator[CharSequence]
    1.25 +  private val char_symbols: Array[String] =
    1.26 +    (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
    1.27 +
    1.28 +  def iterator(text: CharSequence): Iterator[String] =
    1.29 +    new Iterator[String]
    1.30      {
    1.31        private val matcher = new Matcher(text)
    1.32        private var i = 0
    1.33 @@ -96,28 +99,19 @@
    1.34        def next =
    1.35        {
    1.36          val n = matcher(i, text.length)
    1.37 -        val s = text.subSequence(i, i + n)
    1.38 +        val s =
    1.39 +          if (n == 0) ""
    1.40 +          else if (n == 1) {
    1.41 +            val c = text.charAt(i)
    1.42 +            if (c < char_symbols.length) char_symbols(c)
    1.43 +            else text.subSequence(i, i + n).toString
    1.44 +          }
    1.45 +          else text.subSequence(i, i + n).toString
    1.46          i += n
    1.47          s
    1.48        }
    1.49      }
    1.50  
    1.51 -  private val char_symbols: Array[String] =
    1.52 -    (0 until 128).iterator.map(i => new String(Array(i.toChar))).toArray
    1.53 -
    1.54 -  private def make_string(sym: CharSequence): String =
    1.55 -    sym.length match {
    1.56 -      case 0 => ""
    1.57 -      case 1 =>
    1.58 -        val c = sym.charAt(0)
    1.59 -        if (c < char_symbols.length) char_symbols(c)
    1.60 -        else sym.toString
    1.61 -      case _ => sym.toString
    1.62 -    }
    1.63 -
    1.64 -  def iterator_string(text: CharSequence): Iterator[String] =
    1.65 -    iterator(text).map(make_string)
    1.66 -
    1.67  
    1.68    /* decoding offsets */
    1.69  

     2.1 --- a/src/Pure/Thy/html.scala	Tue Jul 05 22:43:18 2011 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Tue Jul 05 23:18:14 2011 +0200
     2.3 @@ -80,7 +80,7 @@
     2.4              flush()
     2.5              ts += elem
     2.6            }
     2.7 -          val syms = Symbol.iterator_string(txt)
     2.8 +          val syms = Symbol.iterator(txt)
     2.9            while (syms.hasNext) {
    2.10              val s1 = syms.next
    2.11              def s2() = if (syms.hasNext) syms.next else ""

     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Jul 05 22:43:18 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jul 05 23:18:14 2011 +0200
     3.3 @@ -124,7 +124,7 @@
     3.4      }
     3.5      var offset = 0
     3.6      var ctrl = ""
     3.7 -    for (sym <- Symbol.iterator_string(text)) {
     3.8 +    for (sym <- Symbol.iterator(text)) {
     3.9        if (ctrl_style(sym).isDefined) ctrl = sym
    3.10        else if (ctrl != "") {
    3.11          if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {