# HG changeset patch # User wenzelm # Date 1301160699 -3600 # Node ID 8223e7f4b0dae35e1b118a7d187e6b796ce4b199 # Parent 12875677300b9cacbb3476be4d23b4a8b77120cd 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; diff -r 12875677300b -r 8223e7f4b0da src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Mar 26 19:16:30 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Mar 26 18:31:39 2011 +0100 @@ -857,7 +857,7 @@ val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p val _ = tracing ("Generated prolog program:\n" ^ prog) val solution = TimeLimit.timeLimit timeout (fn prog => - Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file => + Isabelle_System.with_tmp_file "prolog_file" "" (fn prolog_file => (File.write prolog_file prog; invoke system prolog_file))) prog val _ = tracing ("Prolog returned solution(s):\n" ^ solution) val tss = parse_solutions solution diff -r 12875677300b -r 8223e7f4b0da src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Sat Mar 26 19:16:30 2011 +0100 +++ b/src/Pure/System/isabelle_system.ML Sat Mar 26 18:31:39 2011 +0100 @@ -10,7 +10,8 @@ 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 create_tmp_path: string -> string -> Path.T + val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val with_tmp_dir: string -> (Path.T -> 'a) -> 'a end; @@ -50,30 +51,24 @@ (* unique tmp files *) -local - -fun fresh_path name = +fun create_tmp_path name ext = let - val path = File.tmp_path (Path.basic (name ^ serial_string ())); + val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; -fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path); - -in +fun with_tmp_file name ext f = + let val path = create_tmp_path name ext + in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; -fun with_tmp_file name f = - let val path = fresh_path name - in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; +fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path); fun with_tmp_dir name f = let - val path = fresh_path name; + val path = create_tmp_path name ""; val _ = mkdirs path; in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end; end; -end; - diff -r 12875677300b -r 8223e7f4b0da src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sat Mar 26 19:16:30 2011 +0100 +++ b/src/Pure/Thy/present.ML Sat Mar 26 18:31:39 2011 +0100 @@ -92,9 +92,9 @@ fun display_graph gr = let + val path = Isabelle_System.create_tmp_path "graph" ""; + val _ = write_graph gr path; val _ = writeln "Displaying graph ..."; - val path = File.tmp_path (Path.explode "tmp.graph"); - val _ = write_graph gr path; val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); in () end; @@ -332,21 +332,19 @@ else (); in doc_path end; -fun isabelle_browser graph = +fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir => let - val pdf_path = File.tmp_path graph_pdf_path; - val eps_path = File.tmp_path graph_eps_path; - val gr_path = File.tmp_path graph_path; - val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path; + val pdf_path = Path.append dir graph_pdf_path; + val eps_path = Path.append dir graph_eps_path; + val graph_path = Path.append dir graph_path; + val _ = write_graph graph graph_path; + val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path; in - write_graph graph gr_path; - if Isabelle_System.isabelle_tool "browser" args <> 0 orelse - not (File.exists eps_path) orelse not (File.exists pdf_path) - then error "Failed to prepare dependency graph" - else - let val pdf = File.read pdf_path and eps = File.read eps_path - in File.rm pdf_path; File.rm eps_path; File.rm gr_path; (pdf, eps) end - end; + if Isabelle_System.isabelle_tool "browser" args = 0 andalso + File.exists pdf_path andalso File.exists eps_path + then (File.read pdf_path, File.read eps_path) + else error "Failed to prepare dependency graph" + end); (* finish session -- output all generated text *) @@ -490,9 +488,9 @@ -(** draft document output **) (* FIXME doc_path etc. not thread-safe *) +(** draft document output **) -fun drafts doc_format src_paths = +fun drafts doc_format src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir => let fun prep_draft path i = let @@ -508,8 +506,7 @@ end; val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0)); - val doc_path = File.tmp_path document_path; - val result_path = Path.append doc_path Path.parent; + val doc_path = Path.append dir document_path; val _ = Isabelle_System.mkdirs doc_path; val root_path = Path.append doc_path (Path.basic "root.tex"); val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path; @@ -527,8 +524,11 @@ |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base) |> File.write (Path.append doc_path (tex_path name))); val _ = write_tex_index tex_index doc_path; - in isabelle_document false doc_format documentN "" doc_path result_path end; + val result = isabelle_document false doc_format documentN "" doc_path dir; + val result' = Isabelle_System.create_tmp_path documentN doc_format; + val _ = File.copy result result'; + in result' end); end; diff -r 12875677300b -r 8223e7f4b0da src/Tools/cache_io.ML --- a/src/Tools/cache_io.ML Sat Mar 26 19:16:30 2011 +0100 +++ b/src/Tools/cache_io.ML Sat Mar 26 18:31:39 2011 +0100 @@ -45,8 +45,8 @@ in {output=split_lines out2, redirected_output=out1, return_code=rc} end fun run make_cmd str = - Isabelle_System.with_tmp_file cache_io_prefix (fn in_path => - Isabelle_System.with_tmp_file cache_io_prefix (fn out_path => + Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path => + Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path => raw_run make_cmd str in_path out_path))