# HG changeset patch
# User wenzelm
# Date 1719948940 -7200
# Node ID d327485700697a58be13e2f9fc3b5f9c70be633b
# Parent  59e088605d490a9431946ad91197e01c7ffb9e97
tuned;

diff -r 59e088605d49 -r d32748570069 src/Pure/General/word.scala
--- 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)