--- 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;