elements: more convenient result;

--- 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
     }
   }