--- a/NEWS Sat Feb 27 21:36:58 2021 +0100
+++ b/NEWS Sat Feb 27 22:17:56 2021 +0100
@@ -73,6 +73,7 @@
- Isabelle_System.copy_dir
- Isabelle_System.copy_file
- Isabelle_System.copy_base_file
+ - Isabelle_System.rm_tree
- Isabelle_System.download
--- a/src/Pure/System/isabelle_system.ML Sat Feb 27 21:36:58 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML Sat Feb 27 22:17:56 2021 +0100
@@ -11,13 +11,13 @@
val bash: string -> int
val bash_functions: unit -> string list
val check_bash_function: Proof.context -> string * Position.T -> string
- val rm_tree: Path.T -> unit
val make_directory: Path.T -> Path.T
val copy_dir: Path.T -> Path.T -> unit
val copy_file: Path.T -> Path.T -> unit
val copy_file_base: Path.T * Path.T -> Path.T -> unit
val create_tmp_path: string -> string -> Path.T
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
+ val rm_tree: Path.T -> unit
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
val download: string -> string
end;
@@ -74,11 +74,6 @@
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]; path);
fun copy_dir src dst = scala_function "copy_dir" [src, dst];
@@ -105,6 +100,8 @@
(* tmp dirs *)
+fun rm_tree path = scala_function "rm_tree" [path];
+
fun with_tmp_dir name f =
let val path = create_tmp_path name ""
in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
--- a/src/Pure/System/isabelle_system.scala Sat Feb 27 21:36:58 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Feb 27 22:17:56 2021 +0100
@@ -340,9 +340,7 @@
/* tmp dirs */
- def rm_tree(root: Path): Unit = rm_tree(root.file)
-
- def rm_tree(root: JFile)
+ def rm_tree(root: JFile): Unit =
{
root.delete
if (root.isDirectory) {
@@ -369,6 +367,14 @@
}
}
+ def rm_tree(root: Path): Unit = rm_tree(root.file)
+
+ object Rm_Tree extends Scala.Fun("rm_tree")
+ {
+ val here = Scala_Project.here
+ def apply(arg: String): String = apply_paths1(arg, rm_tree)
+ }
+
def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
--- a/src/Pure/System/scala.scala Sat Feb 27 21:36:58 2021 +0100
+++ b/src/Pure/System/scala.scala Sat Feb 27 22:17:56 2021 +0100
@@ -249,5 +249,6 @@
Isabelle_System.Copy_Dir,
Isabelle_System.Copy_File,
Isabelle_System.Copy_File_Base,
+ Isabelle_System.Rm_Tree,
Isabelle_System.Download,
Isabelle_Tool.Isabelle_Tools)