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;

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

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

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

--- 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))