# HG changeset patch
# User haftmann
# Date 1278574583 -7200
# Node ID 9bb4a74cff4ee480fa394a66715e6548f3aedc66
# Parent  312fe7201f882f86a6c89abf511a6e42b4d5c86b
combinator with_tmp_dir

diff -r 312fe7201f88 -r 9bb4a74cff4e 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 =>