Symbol.explode as in ML;
authorwenzelm
Sat Sep 17 16:19:40 2011 +0200 (2011-09-17)
changeset 44949b49d7f1066c8
parent 44948 b455e4f42c04
child 44950 f60405791a1d
Symbol.explode as in ML;
src/Pure/General/symbol.scala
     1.1 --- a/src/Pure/General/symbol.scala	Sat Sep 17 16:00:54 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Sep 17 16:19:40 2011 +0200
     1.3 @@ -115,6 +115,8 @@
     1.4        }
     1.5      }
     1.6  
     1.7 +  def explode(text: CharSequence): List[Symbol] = iterator(text).toList
     1.8 +
     1.9  
    1.10    /* decoding offsets */
    1.11