--- a/src/Pure/General/symbol.scala Sat Sep 17 16:00:54 2011 +0200
+++ b/src/Pure/General/symbol.scala Sat Sep 17 16:19:40 2011 +0200
@@ -115,6 +115,8 @@
}
}
+ def explode(text: CharSequence): List[Symbol] = iterator(text).toList
+
/* decoding offsets */