# HG changeset patch
# User wenzelm
# Date 1309900694 -7200
# Node ID 8252d51d70e2a1c99e93cb9910abfd81d14575ed
# Parent  3ddaa75c669ce5891b0157e919a4a595dc05a9f4
simplified Symbol.iterator: produce strings, which are mostly preallocated;
eliminated Symbol.CharSequence complications;

diff -r 3ddaa75c669c -r 8252d51d70e2 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jul 05 22:43:18 2011 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jul 05 23:18:14 2011 +0200
@@ -64,11 +64,11 @@
 
   def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
 
-  def is_physical_newline(s: CharSequence): Boolean =
-    "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+  def is_physical_newline(s: String): Boolean =
+    s == "\n" || s == "\r" || s == "\r\n"
 
-  def is_malformed(s: CharSequence): Boolean =
-    !(s.length == 1 && is_plain(s.charAt(0))) && malformed_symbol.pattern.matcher(s).matches
+  def is_malformed(s: String): Boolean =
+    !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
 
   class Matcher(text: CharSequence)
   {
@@ -87,8 +87,11 @@
 
   /* efficient iterators */
 
-  def iterator(text: CharSequence): Iterator[CharSequence] =
-    new Iterator[CharSequence]
+  private val char_symbols: Array[String] =
+    (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
+
+  def iterator(text: CharSequence): Iterator[String] =
+    new Iterator[String]
     {
       private val matcher = new Matcher(text)
       private var i = 0
@@ -96,28 +99,19 @@
       def next =
       {
         val n = matcher(i, text.length)
-        val s = text.subSequence(i, i + n)
+        val s =
+          if (n == 0) ""
+          else if (n == 1) {
+            val c = text.charAt(i)
+            if (c < char_symbols.length) char_symbols(c)
+            else text.subSequence(i, i + n).toString
+          }
+          else text.subSequence(i, i + n).toString
         i += n
         s
       }
     }
 
-  private val char_symbols: Array[String] =
-    (0 until 128).iterator.map(i => new String(Array(i.toChar))).toArray
-
-  private def make_string(sym: CharSequence): String =
-    sym.length match {
-      case 0 => ""
-      case 1 =>
-        val c = sym.charAt(0)
-        if (c < char_symbols.length) char_symbols(c)
-        else sym.toString
-      case _ => sym.toString
-    }
-
-  def iterator_string(text: CharSequence): Iterator[String] =
-    iterator(text).map(make_string)
-
 
   /* decoding offsets */
 
diff -r 3ddaa75c669c -r 8252d51d70e2 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Tue Jul 05 22:43:18 2011 +0200
+++ b/src/Pure/Thy/html.scala	Tue Jul 05 23:18:14 2011 +0200
@@ -80,7 +80,7 @@
             flush()
             ts += elem
           }
-          val syms = Symbol.iterator_string(txt)
+          val syms = Symbol.iterator(txt)
           while (syms.hasNext) {
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""
diff -r 3ddaa75c669c -r 8252d51d70e2 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Jul 05 22:43:18 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jul 05 23:18:14 2011 +0200
@@ -124,7 +124,7 @@
     }
     var offset = 0
     var ctrl = ""
-    for (sym <- Symbol.iterator_string(text)) {
+    for (sym <- Symbol.iterator(text)) {
       if (ctrl_style(sym).isDefined) ctrl = sym
       else if (ctrl != "") {
         if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {