slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
authorwenzelm
Mon Dec 20 14:44:00 2010 +0100 (2010-12-20)
changeset 41307bb8468ae414e
parent 41306 95449e4b4bf6
child 41308 9e576ec5c0dc
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/Pure/System/isabelle_system.ML
src/Tools/Code/code_target.ML
src/Tools/cache_io.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Dec 20 13:36:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Dec 20 14:44:00 2010 +0100
     1.3 @@ -857,8 +857,9 @@
     1.4      val args' = map (rename_vars_term renaming) args
     1.5      val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     1.6      val _ = tracing ("Generated prolog program:\n" ^ prog)
     1.7 -    val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
     1.8 -      (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
     1.9 +    val solution = TimeLimit.timeLimit timeout (fn prog =>
    1.10 +      Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
    1.11 +        (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
    1.12      val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
    1.13      val tss = parse_solutions solution
    1.14    in
     2.1 --- a/src/Pure/System/isabelle_system.ML	Mon Dec 20 13:36:25 2010 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.ML	Mon Dec 20 14:44:00 2010 +0100
     2.3 @@ -7,10 +7,11 @@
     2.4  signature ISABELLE_SYSTEM =
     2.5  sig
     2.6    val isabelle_tool: string -> string -> int
     2.7 -  val rm_tree: Path.T -> unit
     2.8    val mkdirs: Path.T -> unit
     2.9    val mkdir: Path.T -> unit
    2.10    val copy_dir: Path.T -> Path.T -> unit
    2.11 +  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
    2.12 +  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    2.13  end;
    2.14  
    2.15  structure Isabelle_System: ISABELLE_SYSTEM =
    2.16 @@ -37,8 +38,6 @@
    2.17  
    2.18  (* directory operations *)
    2.19  
    2.20 -fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
    2.21 -
    2.22  fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
    2.23  
    2.24  fun mkdir path =
    2.25 @@ -48,5 +47,33 @@
    2.26    if File.eq (src, dst) then ()
    2.27    else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
    2.28  
    2.29 +
    2.30 +(* unique tmp files *)
    2.31 +
    2.32 +local
    2.33 +
    2.34 +fun fresh_path name =
    2.35 +  let
    2.36 +    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
    2.37 +    val _ = File.exists path andalso
    2.38 +      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
    2.39 +  in path end;
    2.40 +
    2.41 +fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
    2.42 +
    2.43 +in
    2.44 +
    2.45 +fun with_tmp_file name f =
    2.46 +  let val path = fresh_path name
    2.47 +  in Exn.release (Exn.capture f path before try File.rm path) end;
    2.48 +
    2.49 +fun with_tmp_dir name f =
    2.50 +  let
    2.51 +    val path = fresh_path name;
    2.52 +    val _ = mkdirs path;
    2.53 +  in Exn.release (Exn.capture f path before try rm_tree path) end;
    2.54 +
    2.55  end;
    2.56  
    2.57 +end;
    2.58 +
     3.1 --- a/src/Tools/Code/code_target.ML	Mon Dec 20 13:36:25 2010 +0100
     3.2 +++ b/src/Tools/Code/code_target.ML	Mon Dec 20 14:44:00 2010 +0100
     3.3 @@ -397,7 +397,7 @@
     3.4      then if strict
     3.5        then error (env_var ^ " not set; cannot check code for " ^ target)
     3.6        else warning (env_var ^ " not set; skipped checking code for " ^ target)
     3.7 -    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
     3.8 +    else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
     3.9    end;
    3.10  
    3.11  end; (* local *)
     4.1 --- a/src/Tools/cache_io.ML	Mon Dec 20 13:36:25 2010 +0100
     4.2 +++ b/src/Tools/cache_io.ML	Mon Dec 20 14:44:00 2010 +0100
     4.3 @@ -7,8 +7,6 @@
     4.4  signature CACHE_IO =
     4.5  sig
     4.6    (*IO wrapper*)
     4.7 -  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
     4.8 -  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
     4.9    type result = {
    4.10      output: string list,
    4.11      redirected_output: string list,
    4.12 @@ -34,21 +32,6 @@
    4.13  
    4.14  val cache_io_prefix = "cache-io-"
    4.15  
    4.16 -fun with_tmp_file name f =
    4.17 -  let
    4.18 -    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
    4.19 -    val x = Exn.capture f path
    4.20 -    val _ = try File.rm path
    4.21 -  in Exn.release x end
    4.22 -
    4.23 -fun with_tmp_dir name f =
    4.24 -  let
    4.25 -    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
    4.26 -    val _ = Isabelle_System.mkdirs path
    4.27 -    val x = Exn.capture f path
    4.28 -    val _ = try Isabelle_System.rm_tree path
    4.29 -  in Exn.release x end
    4.30 -
    4.31  type result = {
    4.32    output: string list,
    4.33    redirected_output: string list,
    4.34 @@ -62,8 +45,9 @@
    4.35    in {output=split_lines out2, redirected_output=out1, return_code=rc} end
    4.36  
    4.37  fun run make_cmd str =
    4.38 -  with_tmp_file cache_io_prefix (fn in_path =>
    4.39 -  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
    4.40 +  Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
    4.41 +    Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
    4.42 +      raw_run make_cmd str in_path out_path))
    4.43  
    4.44  
    4.45  (* cache *)