src/Pure/System/isabelle_system.ML
changeset 41307 bb8468ae414e
parent 40785 c755df0f7062
child 41352 87adb55fb0fb
     1.1 --- a/src/Pure/System/isabelle_system.ML	Mon Dec 20 13:36:25 2010 +0100
     1.2 +++ b/src/Pure/System/isabelle_system.ML	Mon Dec 20 14:44:00 2010 +0100
     1.3 @@ -7,10 +7,11 @@
     1.4  signature ISABELLE_SYSTEM =
     1.5  sig
     1.6    val isabelle_tool: string -> string -> int
     1.7 -  val rm_tree: Path.T -> unit
     1.8    val mkdirs: Path.T -> unit
     1.9    val mkdir: Path.T -> unit
    1.10    val copy_dir: Path.T -> Path.T -> unit
    1.11 +  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
    1.12 +  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    1.13  end;
    1.14  
    1.15  structure Isabelle_System: ISABELLE_SYSTEM =
    1.16 @@ -37,8 +38,6 @@
    1.17  
    1.18  (* directory operations *)
    1.19  
    1.20 -fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
    1.21 -
    1.22  fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
    1.23  
    1.24  fun mkdir path =
    1.25 @@ -48,5 +47,33 @@
    1.26    if File.eq (src, dst) then ()
    1.27    else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
    1.28  
    1.29 +
    1.30 +(* unique tmp files *)
    1.31 +
    1.32 +local
    1.33 +
    1.34 +fun fresh_path name =
    1.35 +  let
    1.36 +    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
    1.37 +    val _ = File.exists path andalso
    1.38 +      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
    1.39 +  in path end;
    1.40 +
    1.41 +fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
    1.42 +
    1.43 +in
    1.44 +
    1.45 +fun with_tmp_file name f =
    1.46 +  let val path = fresh_path name
    1.47 +  in Exn.release (Exn.capture f path before try File.rm path) end;
    1.48 +
    1.49 +fun with_tmp_dir name f =
    1.50 +  let
    1.51 +    val path = fresh_path name;
    1.52 +    val _ = mkdirs path;
    1.53 +  in Exn.release (Exn.capture f path before try rm_tree path) end;
    1.54 +
    1.55  end;
    1.56  
    1.57 +end;
    1.58 +