src/Pure/General/word.scala
changeset 80477 d32748570069
parent 78614 4da5cdaa4dcd
equal deleted inserted replaced
80476:59e088605d49 80477:d32748570069
    64   /* sequence of words */
    64   /* sequence of words */
    65 
    65 
    66   def implode(words: Iterable[String]): String = words.iterator.mkString(" ")
    66   def implode(words: Iterable[String]): String = words.iterator.mkString(" ")
    67 
    67 
    68   def explode(sep: Char => Boolean, text: String): List[String] =
    68   def explode(sep: Char => Boolean, text: String): List[String] =
    69     Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList
    69     List.from(
       
    70       for (s <- Library.separated_chunks(sep, text) if !s.isEmpty)
       
    71         yield s.toString)
    70 
    72 
    71   def explode(sep: Char, text: String): List[String] =
    73   def explode(sep: Char, text: String): List[String] =
    72     explode(_ == sep, text)
    74     explode(_ == sep, text)
    73 
    75 
    74   def explode(text: String): List[String] =
    76   def explode(text: String): List[String] =