more Isabelle/ML/Scala operations;
clarified errors;

--- a/NEWS	Sat Feb 27 20:49:38 2021 +0100
+++ b/NEWS	Sat Feb 27 21:01:07 2021 +0100
@@ -66,6 +66,14 @@
 available, CPU time is only available on Linux and macOS, GC time is
 unavailable.
 
+* Likewise, the following Isabelle/ML system operations are run in the
+context of Isabelle/Scala:
+
+  - Isabelle_System.make_directory
+  - Isabelle_System.copy_dir
+  - Isabelle_System.copy_file
+  - Isabelle_System.copy_base_file
+
 
 
 New in Isabelle2021 (February 2021)

--- a/src/Pure/System/isabelle_system.ML	Sat Feb 27 20:49:38 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Feb 27 21:01:07 2021 +0100
@@ -69,39 +69,24 @@
     (bash_functions () |> map (rpair Position.none)) ctxt arg;
 
 
-(* directory operations *)
+(* directory and file operations *)
+
+fun scala_function name args =
+  ignore (Scala.function name (space_implode "\000" (map (Path.implode o File.absolute_path) args)));
 
 fun system_command cmd =
   if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
 
 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
 
-fun make_directory path =
-  (Scala.function "make_directory" (Path.implode (File.absolute_path path)); path);
+fun make_directory path = (scala_function "make_directory" [path]; path);
 
-fun copy_dir src dst =
-  if File.eq (src, dst) then ()
-  else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
+fun copy_dir src dst = scala_function "copy_dir" [src, dst];
 
-fun copy_file src0 dst0 =
-  let
-    val src = Path.expand src0;
-    val dst = Path.expand dst0;
-    val target = if File.is_dir dst then dst + Path.base src else dst;
-  in
-    if File.eq (src, target) then ()
-    else
-      ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target))
-  end;
+fun copy_file src dst = scala_function "copy_file" [src, dst];
 
-fun copy_file_base (base_dir, src0) target_dir =
-  let
-    val src = Path.expand src0;
-    val src_dir = Path.dir src;
-    val _ =
-      if Path.starts_basic src then ()
-      else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
-  in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end;
+fun copy_file_base (base_dir, src) target_dir =
+  scala_function "copy_file_base" [base_dir, src, target_dir];
 
 
 (* tmp files *)

--- a/src/Pure/System/isabelle_system.scala	Sat Feb 27 20:49:38 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 27 21:01:07 2021 +0100
@@ -180,6 +180,21 @@
 
   /** file-system operations **/
 
+  /* scala functions */
+
+  private def apply_paths(arg: String, fun: List[Path] => Unit): String =
+    { fun(Library.space_explode('\u0000', 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) })
+
+
   /* permissions */
 
   def chmod(arg: String, path: Path): Unit =
@@ -198,30 +213,48 @@
     path
   }
 
-  object Make_Directory extends Scala.Fun("make_directory")
-  {
-    val here = Scala_Project.here
-    def apply(arg: String): String = { make_directory(Path.explode(arg)); "" }
-  }
-
   def new_directory(path: Path): Path =
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)
 
+  def copy_dir(dir1: Path, dir2: Path): Unit =
+  {
+    val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
+    if (!res.ok) {
+      cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
+    }
+  }
 
 
-  /* copy */
+  object Make_Directory extends Scala.Fun("make_directory")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String = apply_paths1(arg, make_directory)
+  }
 
-  def copy_dir(dir1: Path, dir2: Path): Unit =
-    bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
+  object Copy_Dir extends Scala.Fun("copy_dir")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String = apply_paths2(arg, copy_dir)
+  }
+
+
+  /* copy files */
 
   def copy_file(src: JFile, dst: JFile): Unit =
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target)) {
-      Files.copy(src.toPath, target.toPath,
-        StandardCopyOption.COPY_ATTRIBUTES,
-        StandardCopyOption.REPLACE_EXISTING)
+      try {
+        Files.copy(src.toPath, target.toPath,
+          StandardCopyOption.COPY_ATTRIBUTES,
+          StandardCopyOption.REPLACE_EXISTING)
+      }
+      catch {
+        case ERROR(msg) =>
+          cat_error("Failed top copy file " +
+            File.path(src).absolute + " to " + File.path(dst).absolute, msg)
+      }
     }
   }
 
@@ -236,7 +269,20 @@
   }
 
 
-  /* move */
+  object Copy_File extends Scala.Fun("copy_file")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String = apply_paths2(arg, copy_file)
+  }
+
+  object Copy_File_Base extends Scala.Fun("copy_file_base")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String = apply_paths3(arg, copy_file_base)
+  }
+
+
+  /* move files */
 
   def move_file(src: JFile, dst: JFile)
   {

--- a/src/Pure/System/scala.scala	Sat Feb 27 20:49:38 2021 +0100
+++ b/src/Pure/System/scala.scala	Sat Feb 27 21:01:07 2021 +0100
@@ -246,4 +246,7 @@
   Bash.Process,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,
+  Isabelle_System.Copy_Dir,
+  Isabelle_System.Copy_File,
+  Isabelle_System.Copy_File_Base,
   Isabelle_Tool.Isabelle_Tools)