# HG changeset patch
# User wenzelm
# Date 1260137213 -3600
# Node ID 6e5eafb373b38abcf0051cc5ea8f1055c3040382
# Parent  1fecda9486972b25ef4be5d80c1852b4d5fee060
elements: more convenient result;

diff -r 1fecda948697 -r 6e5eafb373b3 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Dec 06 22:23:31 2009 +0100
+++ b/src/Pure/General/symbol.scala	Sun Dec 06 23:06:53 2009 +0100
@@ -45,7 +45,7 @@
   private def could_open(c: Char): Boolean =
     c == '\\' || Character.isHighSurrogate(c)
 
-  def elements(text: CharSequence) = new Iterator[CharSequence] {
+  def elements(text: CharSequence) = new Iterator[String] {
     private val matcher = regex.pattern.matcher(text)
     private var i = 0
     def hasNext = i < text.length
@@ -58,7 +58,7 @@
         else 1
       val s = text.subSequence(i, i + len)
       i += len
-      s
+      s.toString
     }
   }