--- 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;
+