src/Pure/General/symbol.scala
changeset 44949 b49d7f1066c8
parent 44238 36120feb70ed
child 44992 aa34d2d049ce
     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