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