# HG changeset patch
# User wenzelm
# Date 1292852640 -3600
# Node ID bb8468ae414eb737cee62e5bd90fcf32d6440acf
# Parent  95449e4b4bf6dc2c0b61ac69703b26be6e19eb01
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;

diff -r 95449e4b4bf6 -r bb8468ae414e src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Dec 20 13:36:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Dec 20 14:44:00 2010 +0100
@@ -857,8 +857,9 @@
     val args' = map (rename_vars_term renaming) args
     val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     val _ = tracing ("Generated prolog program:\n" ^ prog)
-    val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
-      (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
+    val solution = TimeLimit.timeLimit timeout (fn prog =>
+      Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
+        (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
     val tss = parse_solutions solution
   in
diff -r 95449e4b4bf6 -r bb8468ae414e src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Dec 20 13:36:25 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Dec 20 14:44:00 2010 +0100
@@ -7,10 +7,11 @@
 signature ISABELLE_SYSTEM =
 sig
   val isabelle_tool: string -> string -> int
-  val rm_tree: Path.T -> unit
   val mkdirs: Path.T -> unit
   val mkdir: Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
+  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -37,8 +38,6 @@
 
 (* directory operations *)
 
-fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
-
 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
 
 fun mkdir path =
@@ -48,5 +47,33 @@
   if File.eq (src, dst) then ()
   else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
 
+
+(* unique tmp files *)
+
+local
+
+fun fresh_path name =
+  let
+    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
+    val _ = File.exists path andalso
+      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
+  in path end;
+
+fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+
+in
+
+fun with_tmp_file name f =
+  let val path = fresh_path name
+  in Exn.release (Exn.capture f path before try File.rm path) end;
+
+fun with_tmp_dir name f =
+  let
+    val path = fresh_path name;
+    val _ = mkdirs path;
+  in Exn.release (Exn.capture f path before try rm_tree path) end;
+
 end;
 
+end;
+
diff -r 95449e4b4bf6 -r bb8468ae414e src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Dec 20 13:36:25 2010 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Dec 20 14:44:00 2010 +0100
@@ -397,7 +397,7 @@
     then if strict
       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)
-    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
+    else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
 end; (* local *)
diff -r 95449e4b4bf6 -r bb8468ae414e src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Mon Dec 20 13:36:25 2010 +0100
+++ b/src/Tools/cache_io.ML	Mon Dec 20 14:44:00 2010 +0100
@@ -7,8 +7,6 @@
 signature CACHE_IO =
 sig
   (*IO wrapper*)
-  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
-  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   type result = {
     output: string list,
     redirected_output: string list,
@@ -34,21 +32,6 @@
 
 val cache_io_prefix = "cache-io-"
 
-fun with_tmp_file name f =
-  let
-    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val x = Exn.capture f path
-    val _ = try File.rm path
-  in Exn.release x end
-
-fun with_tmp_dir name f =
-  let
-    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val _ = Isabelle_System.mkdirs path
-    val x = Exn.capture f path
-    val _ = try Isabelle_System.rm_tree path
-  in Exn.release x end
-
 type result = {
   output: string list,
   redirected_output: string list,
@@ -62,8 +45,9 @@
   in {output=split_lines out2, redirected_output=out1, return_code=rc} end
 
 fun run make_cmd str =
-  with_tmp_file cache_io_prefix (fn in_path =>
-  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
+  Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
+    Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
+      raw_run make_cmd str in_path out_path))
 
 
 (* cache *)