src/Pure/System/isabelle_system.scala

 
   /** file-system operations **/
 
   /* scala functions */
 
-  private def apply_paths(arg: String, fun: List[Path] => Unit): String =
-    { 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) })
-
-  private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String =
-    apply_paths(arg, { 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_paths(args: List[String], fun: List[Path] => Unit): List[String] =
+    { fun(args.map(Path.explode)); Nil }
+
+  private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
+    apply_paths(args, { case List(path) => fun(path) })
+
+  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(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
+    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
 
   def chmod(arg: String, path: Path): Unit =

       cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
     }
   }
 
 
-  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)
-  }
-
-  object Copy_Dir extends Scala.Fun_String("copy_dir")
+    def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
+  }
+
+  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)
   }
 
 
   /* copy files */
 

     if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
     copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
   }
 
 
-  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)
-  }
-
-  object Copy_File_Base extends Scala.Fun_String("copy_file_base")
+    def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
+  }
+
+  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)
   }
 
 
   /* move files */
 

     }
   }
 
   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 =
   {
     val dir = Files.createTempDirectory(base_dir.toPath, name).toFile