Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
authorwenzelm
Sat Mar 26 18:31:39 2011 +0100 (2011-03-26)
changeset 421278223e7f4b0da
parent 42126 12875677300b
child 42128 eb84d28961a9
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/Pure/System/isabelle_system.ML
src/Pure/Thy/present.ML
src/Tools/cache_io.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Mar 26 19:16:30 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Mar 26 18:31:39 2011 +0100
     1.3 @@ -857,7 +857,7 @@
     1.4      val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     1.5      val _ = tracing ("Generated prolog program:\n" ^ prog)
     1.6      val solution = TimeLimit.timeLimit timeout (fn prog =>
     1.7 -      Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
     1.8 +      Isabelle_System.with_tmp_file "prolog_file" "" (fn prolog_file =>
     1.9          (File.write prolog_file prog; invoke system prolog_file))) prog
    1.10      val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
    1.11      val tss = parse_solutions solution
     2.1 --- a/src/Pure/System/isabelle_system.ML	Sat Mar 26 19:16:30 2011 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.ML	Sat Mar 26 18:31:39 2011 +0100
     2.3 @@ -10,7 +10,8 @@
     2.4    val mkdirs: Path.T -> unit
     2.5    val mkdir: Path.T -> unit
     2.6    val copy_dir: Path.T -> Path.T -> unit
     2.7 -  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
     2.8 +  val create_tmp_path: string -> string -> Path.T
     2.9 +  val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
    2.10    val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    2.11  end;
    2.12  
    2.13 @@ -50,30 +51,24 @@
    2.14  
    2.15  (* unique tmp files *)
    2.16  
    2.17 -local
    2.18 -
    2.19 -fun fresh_path name =
    2.20 +fun create_tmp_path name ext =
    2.21    let
    2.22 -    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
    2.23 +    val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext);
    2.24      val _ = File.exists path andalso
    2.25        raise Fail ("Temporary file already exists: " ^ Path.print path);
    2.26    in path end;
    2.27  
    2.28 -fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
    2.29 -
    2.30 -in
    2.31 +fun with_tmp_file name ext f =
    2.32 +  let val path = create_tmp_path name ext
    2.33 +  in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
    2.34  
    2.35 -fun with_tmp_file name f =
    2.36 -  let val path = fresh_path name
    2.37 -  in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
    2.38 +fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
    2.39  
    2.40  fun with_tmp_dir name f =
    2.41    let
    2.42 -    val path = fresh_path name;
    2.43 +    val path = create_tmp_path name "";
    2.44      val _ = mkdirs path;
    2.45    in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
    2.46  
    2.47  end;
    2.48  
    2.49 -end;
    2.50 -
     3.1 --- a/src/Pure/Thy/present.ML	Sat Mar 26 19:16:30 2011 +0100
     3.2 +++ b/src/Pure/Thy/present.ML	Sat Mar 26 18:31:39 2011 +0100
     3.3 @@ -92,9 +92,9 @@
     3.4  
     3.5  fun display_graph gr =
     3.6    let
     3.7 +    val path = Isabelle_System.create_tmp_path "graph" "";
     3.8 +    val _ = write_graph gr path;
     3.9      val _ = writeln "Displaying graph ...";
    3.10 -    val path = File.tmp_path (Path.explode "tmp.graph");
    3.11 -    val _ = write_graph gr path;
    3.12      val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    3.13    in () end;
    3.14  
    3.15 @@ -332,21 +332,19 @@
    3.16        else ();
    3.17    in doc_path end;
    3.18  
    3.19 -fun isabelle_browser graph =
    3.20 +fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir =>
    3.21    let
    3.22 -    val pdf_path = File.tmp_path graph_pdf_path;
    3.23 -    val eps_path = File.tmp_path graph_eps_path;
    3.24 -    val gr_path = File.tmp_path graph_path;
    3.25 -    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
    3.26 +    val pdf_path = Path.append dir graph_pdf_path;
    3.27 +    val eps_path = Path.append dir graph_eps_path;
    3.28 +    val graph_path = Path.append dir graph_path;
    3.29 +    val _ = write_graph graph graph_path;
    3.30 +    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
    3.31    in
    3.32 -    write_graph graph gr_path;
    3.33 -    if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
    3.34 -      not (File.exists eps_path) orelse not (File.exists pdf_path)
    3.35 -    then error "Failed to prepare dependency graph"
    3.36 -    else
    3.37 -      let val pdf = File.read pdf_path and eps = File.read eps_path
    3.38 -      in File.rm pdf_path; File.rm eps_path; File.rm gr_path; (pdf, eps) end
    3.39 -  end;
    3.40 +    if Isabelle_System.isabelle_tool "browser" args = 0 andalso
    3.41 +      File.exists pdf_path andalso File.exists eps_path
    3.42 +    then (File.read pdf_path, File.read eps_path)
    3.43 +    else error "Failed to prepare dependency graph"
    3.44 +  end);
    3.45  
    3.46  
    3.47  (* finish session -- output all generated text *)
    3.48 @@ -490,9 +488,9 @@
    3.49  
    3.50  
    3.51  
    3.52 -(** draft document output **)  (* FIXME doc_path etc. not thread-safe *)
    3.53 +(** draft document output **)
    3.54  
    3.55 -fun drafts doc_format src_paths =
    3.56 +fun drafts doc_format src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
    3.57    let
    3.58      fun prep_draft path i =
    3.59        let
    3.60 @@ -508,8 +506,7 @@
    3.61        end;
    3.62      val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
    3.63  
    3.64 -    val doc_path = File.tmp_path document_path;
    3.65 -    val result_path = Path.append doc_path Path.parent;
    3.66 +    val doc_path = Path.append dir document_path;
    3.67      val _ = Isabelle_System.mkdirs doc_path;
    3.68      val root_path = Path.append doc_path (Path.basic "root.tex");
    3.69      val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
    3.70 @@ -527,8 +524,11 @@
    3.71        |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
    3.72        |> File.write (Path.append doc_path (tex_path name)));
    3.73      val _ = write_tex_index tex_index doc_path;
    3.74 -  in isabelle_document false doc_format documentN "" doc_path result_path end;
    3.75  
    3.76 +    val result = isabelle_document false doc_format documentN "" doc_path dir;
    3.77 +    val result' = Isabelle_System.create_tmp_path documentN doc_format;
    3.78 +    val _ = File.copy result result';
    3.79 +  in result' end);
    3.80  
    3.81  end;
    3.82  
     4.1 --- a/src/Tools/cache_io.ML	Sat Mar 26 19:16:30 2011 +0100
     4.2 +++ b/src/Tools/cache_io.ML	Sat Mar 26 18:31:39 2011 +0100
     4.3 @@ -45,8 +45,8 @@
     4.4    in {output=split_lines out2, redirected_output=out1, return_code=rc} end
     4.5  
     4.6  fun run make_cmd str =
     4.7 -  Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
     4.8 -    Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
     4.9 +  Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
    4.10 +    Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
    4.11        raw_run make_cmd str in_path out_path))
    4.12  
    4.13