--- a/src/Pure/General/word.scala Tue Jul 02 17:38:28 2024 +0200
+++ b/src/Pure/General/word.scala Tue Jul 02 21:35:40 2024 +0200
@@ -66,7 +66,9 @@
def implode(words: Iterable[String]): String = words.iterator.mkString(" ")
def explode(sep: Char => Boolean, text: String): List[String] =
- Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList
+ List.from(
+ for (s <- Library.separated_chunks(sep, text) if !s.isEmpty)
+ yield s.toString)
def explode(sep: Char, text: String): List[String] =
explode(_ == sep, text)