clarified signature;

--- a/src/Pure/System/bash.scala	Mon Mar 01 17:44:44 2021 +0100
+++ b/src/Pure/System/bash.scala	Mon Mar 01 18:11:06 2021 +0100
@@ -223,11 +223,12 @@
         case _ if is_interrupt => ""
         case Exn.Exn(exn) => Exn.message(exn)
         case Exn.Res(res) =>
-         (res.rc.toString ::
-          res.timing.elapsed.ms.toString ::
-          res.timing.cpu.ms.toString ::
-          res.out_lines.length.toString ::
-          res.out_lines ::: res.err_lines).mkString("\u0000")
+          Library.cat_strings0(
+            res.rc.toString ::
+            res.timing.elapsed.ms.toString ::
+            res.timing.cpu.ms.toString ::
+            res.out_lines.length.toString ::
+            res.out_lines ::: res.err_lines)
       }
     }
   }

--- a/src/Pure/System/isabelle_system.ML	Mon Mar 01 17:44:44 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Mar 01 18:11:06 2021 +0100
@@ -30,7 +30,7 @@
 fun bash_process script =
   Scala.function_thread "bash_process"
     ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
-  |> space_explode "\000"
+  |> split_strings0
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
       | a :: b :: c :: d :: lines =>
@@ -72,7 +72,7 @@
 (* directory and file operations *)
 
 val absolute_path = Path.implode o File.absolute_path;
-fun scala_function0 name = ignore o Scala.function name o space_implode "\000";
+fun scala_function0 name = ignore o Scala.function name o cat_strings0;
 fun scala_function name = scala_function0 name o map absolute_path;
 
 fun make_directory path = (scala_function "make_directory" [path]; path);

--- a/src/Pure/System/isabelle_system.scala	Mon Mar 01 17:44:44 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 01 18:11:06 2021 +0100
@@ -129,7 +129,7 @@
           if (rc != 0) error(output)
 
           val entries =
-            (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
+            (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield {
               val i = entry.indexOf('=')
               if (i <= 0) entry -> ""
               else entry.substring(0, i) -> entry.substring(i + 1)
@@ -183,7 +183,7 @@
   /* scala functions */
 
   private def apply_paths(arg: String, fun: List[Path] => Unit): String =
-    { fun(Library.space_explode('\u0000', arg).map(Path.explode)); "" }
+    { fun(Library.split_strings0(arg).map(Path.explode)); "" }
 
   private def apply_paths1(arg: String, fun: Path => Unit): String =
     apply_paths(arg, { case List(path) => fun(path) })
@@ -568,7 +568,7 @@
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
-      Library.space_explode('\u0000', arg) match {
+      Library.split_strings0(arg) match {
         case List(url, file) => download(url, Path.explode(file)); ""
       }
   }

--- a/src/Pure/library.ML	Mon Mar 01 17:44:44 2021 +0100
+++ b/src/Pure/library.ML	Mon Mar 01 18:11:06 2021 +0100
@@ -143,6 +143,8 @@
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
+  val cat_strings0: string list -> string
+  val split_strings0: string -> string list
   val plain_words: string -> string
   val prefix_lines: string -> string -> string
   val prefix: string -> string -> string
@@ -739,6 +741,9 @@
 
 val split_lines = space_explode "\n";
 
+val cat_strings0 = space_implode "\000";
+val split_strings0 = space_explode "\000";
+
 fun plain_words s = space_explode "_" s |> space_implode " ";
 
 fun prefix_lines "" txt = txt

--- a/src/Pure/library.scala	Mon Mar 01 17:44:44 2021 +0100
+++ b/src/Pure/library.scala	Mon Mar 01 18:11:06 2021 +0100
@@ -126,6 +126,9 @@
 
   /* strings */
 
+  def cat_strings0(strs: TraversableOnce[String]): String = strs.mkString("\u0000")
+  def split_strings0(str: String): List[String] = space_explode('\u0000', str)
+
   def make_string(f: StringBuilder => Unit): String =
   {
     val s = new StringBuilder