# HG changeset patch # User wenzelm # Date 1614456067 -3600 # Node ID 5b15eee1a661bd8f967f77ee9f7d89487cddf6bc # Parent 0b8411b27059be92c6877747d483313d60c14cd4 more Isabelle/ML/Scala operations; clarified errors; diff -r 0b8411b27059 -r 5b15eee1a661 NEWS --- 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) diff -r 0b8411b27059 -r 5b15eee1a661 src/Pure/System/isabelle_system.ML --- 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 *) diff -r 0b8411b27059 -r 5b15eee1a661 src/Pure/System/isabelle_system.scala --- 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) { diff -r 0b8411b27059 -r 5b15eee1a661 src/Pure/System/scala.scala --- 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)