combinator with_tmp_dir
authorhaftmann
Thu, 08 Jul 2010 09:36:23 +0200
changeset 37740 9bb4a74cff4e
parent 37739 312fe7201f88
child 37741 763feb2abb0d
combinator with_tmp_dir
src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Thu Jul 08 09:36:22 2010 +0200
+++ b/src/Tools/cache_io.ML	Thu Jul 08 09:36:23 2010 +0200
@@ -7,6 +7,7 @@
 signature CACHE_IO =
 sig
   val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val run: (Path.T -> Path.T -> string) -> string -> string list * string list
 
   type cache
@@ -31,6 +32,14 @@
     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 _ = File.mkdir path
+    val x = Exn.capture f path
+    val _ = try File.rm_tree path
+  in Exn.release x end
+
 fun run make_cmd str =
   with_tmp_file cache_io_prefix (fn in_path =>
   with_tmp_file cache_io_prefix (fn out_path =>