# HG changeset patch
# User wenzelm
# Date 1316269180 -7200
# Node ID b49d7f1066c8b7eb0a657a70b1cfc260bd340089
# Parent  b455e4f42c0401af086a48584c804f2cea20fa0a
Symbol.explode as in ML;

diff -r b455e4f42c04 -r b49d7f1066c8 src/Pure/General/symbol.scala
--- 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 */