tuned iteration over short symbols;

--- a/src/Pure/General/symbol.scala	Tue Jun 21 12:53:55 2011 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jun 21 13:29:44 2011 +0200
@@ -85,21 +85,38 @@
   }
 
 
-  /* iterator */
+  /* efficient iterators */
 
-  def iterator(text: CharSequence) = new Iterator[CharSequence]
-  {
-    private val matcher = new Matcher(text)
-    private var i = 0
-    def hasNext = i < text.length
-    def next =
+  def iterator(text: CharSequence): Iterator[CharSequence] =
+    new Iterator[CharSequence]
     {
-      val n = matcher(i, text.length)
-      val s = text.subSequence(i, i + n)
-      i += n
-      s
+      private val matcher = new Matcher(text)
+      private var i = 0
+      def hasNext = i < text.length
+      def next =
+      {
+        val n = matcher(i, text.length)
+        val s = text.subSequence(i, i + n)
+        i += n
+        s
+      }
     }
-  }
+
+  private val char_symbols: Array[String] =
+    (0 to 127).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 */

--- a/src/Pure/Thy/html.scala	Tue Jun 21 12:53:55 2011 +0200
+++ b/src/Pure/Thy/html.scala	Tue Jun 21 13:29:44 2011 +0200
@@ -73,7 +73,7 @@
             flush()
             ts += elem
           }
-          val syms = Symbol.iterator(txt).map(_.toString)
+          val syms = Symbol.iterator_string(txt)
           while (syms.hasNext) {
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""

--- a/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 12:53:55 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 13:29:44 2011 +0200
@@ -90,7 +90,7 @@
     }
     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)) {