# HG changeset patch
# User wenzelm
# Date 1618256884 -7200
# Node ID 355af2d1b81780288e5fcc75f90ad9c47ef1dd62
# Parent  4e6b31ed71970a6fe86a9e96857dbd41f2b69e30
clarified signature;

diff -r 4e6b31ed7197 -r 355af2d1b817 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Apr 12 18:29:34 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Mon Apr 12 21:48:04 2021 +0200
@@ -78,8 +78,7 @@
 (* directory and file operations *)
 
 val absolute_path = Path.implode o File.absolute_path;
-fun scala_function0 name = ignore o Scala.function1 name o cat_strings0;
-fun scala_function name = scala_function0 name o map absolute_path;
+fun scala_function name = ignore o Scala.function name o map absolute_path;
 
 fun make_directory path = (scala_function "make_directory" [path]; path);
 
@@ -88,8 +87,8 @@
 fun copy_file src dst = scala_function "copy_file" [src, dst];
 
 fun copy_file_base (base_dir, src) target_dir =
-  scala_function0 "copy_file_base"
-    [absolute_path base_dir, Path.implode src, absolute_path target_dir];
+  ignore (Scala.function "copy_file_base"
+    [absolute_path base_dir, Path.implode src, absolute_path target_dir]);
 
 
 (* tmp files *)
diff -r 4e6b31ed7197 -r 355af2d1b817 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Apr 12 18:29:34 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Apr 12 21:48:04 2021 +0200
@@ -227,17 +227,17 @@
 
   /* scala functions */
 
-  private def apply_paths(arg: String, fun: List[Path] => Unit): String =
-    { fun(Library.split_strings0(arg).map(Path.explode)); "" }
+  private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] =
+    { fun(args.map(Path.explode)); Nil }
 
-  private def apply_paths1(arg: String, fun: Path => Unit): String =
-    apply_paths(arg, { case List(path) => fun(path) })
+  private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
+    apply_paths(args, { case List(path) => fun(path) })
 
-  private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String =
-    apply_paths(arg, { case List(path1, path2) => fun(path1, path2) })
+  private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
+    apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
 
-  private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String =
-    apply_paths(arg, { case List(path1, path2, path3) => fun(path1, path2, path3) })
+  private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
+    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
@@ -273,16 +273,16 @@
   }
 
 
-  object Make_Directory extends Scala.Fun_String("make_directory")
+  object Make_Directory extends Scala.Fun_Strings("make_directory")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths1(arg, make_directory)
+    def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
   }
 
-  object Copy_Dir extends Scala.Fun_String("copy_dir")
+  object Copy_Dir extends Scala.Fun_Strings("copy_dir")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths2(arg, copy_dir)
+    def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
   }
 
 
@@ -316,16 +316,16 @@
   }
 
 
-  object Copy_File extends Scala.Fun_String("copy_file")
+  object Copy_File extends Scala.Fun_Strings("copy_file")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths2(arg, copy_file)
+    def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
   }
 
-  object Copy_File_Base extends Scala.Fun_String("copy_file_base")
+  object Copy_File_Base extends Scala.Fun_Strings("copy_file_base")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths3(arg, copy_file_base)
+    def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
   }
 
 
@@ -416,10 +416,10 @@
 
   def rm_tree(root: Path): Unit = rm_tree(root.file)
 
-  object Rm_Tree extends Scala.Fun_String("rm_tree")
+  object Rm_Tree extends Scala.Fun_Strings("rm_tree")
   {
     val here = Scala_Project.here
-    def apply(arg: String): String = apply_paths1(arg, rm_tree)
+    def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
   }
 
   def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =