# HG changeset patch
# User wenzelm
# Date 1614460676 -3600
# Node ID 48abb09d49ea728f07e418bcb5e656d595c6169c
# Parent  c2ab1a970e82500bf8f874649df12b8aad5c1ce8
more Isabelle/ML/Scala operations;

diff -r c2ab1a970e82 -r 48abb09d49ea NEWS
--- 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
 
 
diff -r c2ab1a970e82 -r 48abb09d49ea src/Pure/System/isabelle_system.ML
--- 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;
diff -r c2ab1a970e82 -r 48abb09d49ea src/Pure/System/isabelle_system.scala
--- 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
diff -r c2ab1a970e82 -r 48abb09d49ea src/Pure/System/scala.scala
--- 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)