# HG changeset patch
# User wenzelm
# Date 1422218781 -3600
# Node ID 2c27c3d1fd3bd84386c03b58df378e64e4083ad4
# Parent  d57e275b2d82b11f5fe6d721a67d484104dce398
provide session_graph.pdf via Isabelle/Scala;

diff -r d57e275b2d82 -r 2c27c3d1fd3b src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Sun Jan 25 20:22:20 2015 +0100
+++ b/src/Pure/PIDE/session.ML	Sun Jan 25 21:46:21 2015 +0100
@@ -10,7 +10,7 @@
   val welcome: unit -> string
   val get_keywords: unit -> Keyword.keywords
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
-    (Path.T * Path.T) list -> string -> string * string -> bool -> unit
+    (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
   val shutdown: unit -> unit
   val finish: unit -> unit
   val save: string -> unit
@@ -42,7 +42,7 @@
 
 (* init *)
 
-fun init build info info_path doc doc_graph doc_output doc_variants doc_files
+fun init build info info_path doc doc_graph doc_output doc_variants doc_files graph_file
     parent (chapter, name) verbose =
   if #name (! session) <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
@@ -52,7 +52,7 @@
       val _ = session_finished := false;
     in
       Present.init build info info_path (if doc = "false" then "" else doc)
-        doc_graph doc_output doc_variants doc_files (chapter, name)
+        doc_graph doc_output doc_variants doc_files graph_file (chapter, name)
         verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
     end;
 
diff -r d57e275b2d82 -r 2c27c3d1fd3b src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Jan 25 20:22:20 2015 +0100
+++ b/src/Pure/Thy/present.ML	Sun Jan 25 21:46:21 2015 +0100
@@ -10,8 +10,8 @@
   val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
-    (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
-  val finish: unit -> unit  (*not thread-safe!*)
+    (Path.T * Path.T) list -> Path.T -> string * string -> bool -> theory list -> unit
+  val finish: unit -> unit
   val theory_output: string -> string -> unit
   val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
   val display_drafts: Path.T list -> int
@@ -34,7 +34,6 @@
 val doc_indexN = "session";
 val graph_path = Path.basic "session.graph";
 val graph_pdf_path = Path.basic "session_graph.pdf";
-val graph_eps_path = Path.basic "session_graph.eps";
 
 fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
 
@@ -163,16 +162,16 @@
 type session_info =
   {name: string, chapter: string, info_path: Path.T, info: bool,
     doc_format: string, doc_graph: bool, doc_output: Path.T option,
-    doc_files: (Path.T * Path.T) list, documents: (string * string) list,
+    doc_files: (Path.T * Path.T) list, graph_file: Path.T, documents: (string * string) list,
     verbose: bool, readme: Path.T option};
 
 fun make_session_info
   (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
-    doc_files, documents, verbose, readme) =
+    doc_files, graph_file, documents, verbose, readme) =
   {name = name, chapter = chapter, info_path = info_path, info = info,
     doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
-    doc_files = doc_files, documents = documents, verbose = verbose,
-    readme = readme}: session_info;
+    doc_files = doc_files, graph_file = graph_file, documents = documents,
+    verbose = verbose, readme = readme}: session_info;
 
 
 (* state *)
@@ -206,7 +205,7 @@
 
 (* init session *)
 
-fun init build info info_path doc doc_graph document_output doc_variants doc_files
+fun init build info info_path doc doc_graph document_output doc_variants doc_files graph_file
     (chapter, name) verbose thys =
   if not build andalso not info andalso doc = "" then
     (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
@@ -230,7 +229,7 @@
     in
       session_info :=
         SOME (make_session_info (name, chapter, info_path, info, doc,
-          doc_graph, doc_output, doc_files, documents, verbose, readme));
+          doc_graph, doc_output, doc_files, graph_file, documents, verbose, readme));
       Synchronized.change browser_info (K (init_browser_info (chapter, name) thys));
       add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
     end;
@@ -252,20 +251,6 @@
       else ();
   in doc_path end;
 
-fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir =>
-  let
-    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 _ = Graph_Display.write_graph_browser graph_path graph;
-    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
-  in
-    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 *)
 
@@ -280,10 +265,11 @@
 
 fun finish () =
   with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
-    doc_output, doc_files, documents, verbose, readme, ...} =>
+    doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
   let
     val {theories, tex_index, html_index, graph} = Synchronized.value browser_info;
     val thys = Symtab.dest theories;
+    val sorted_graph = Graph_Display.sort_graph graph;
 
     val chapter_prefix = Path.append info_path (Path.basic chapter);
     val session_prefix = Path.append chapter_prefix (Path.basic name);
@@ -291,12 +277,6 @@
     fun finish_html (a, {html_source, ...}: theory_info) =
       File.write (Path.append session_prefix (html_path a)) html_source;
 
-    val sorted_graph = Graph_Display.sort_graph graph;
-    val opt_graphs =
-      if doc_graph andalso not (null documents) then
-        SOME (isabelle_browser sorted_graph)
-      else NONE;
-
     val _ =
       if info then
        (Isabelle_System.mkdirs session_prefix;
@@ -323,12 +303,7 @@
           Isabelle_System.isabelle_tool "latex"
             ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
         val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
-        val _ =
-          (case opt_graphs of
-            NONE => ()
-          | SOME (pdf, eps) =>
-              (File.write (Path.append doc_dir graph_pdf_path) pdf;
-                File.write (Path.append doc_dir graph_eps_path) eps));
+        val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir graph_pdf_path);
         val _ = write_tex_index tex_index doc_dir;
         val _ =
           List.app (fn (a, {tex_source, ...}) =>
diff -r d57e275b2d82 -r 2c27c3d1fd3b src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun Jan 25 20:22:20 2015 +0100
+++ b/src/Pure/Tools/build.ML	Sun Jan 25 21:46:21 2015 +0100
@@ -124,12 +124,12 @@
       val _ = SHA1_Samples.test ();
 
       val (command_timings, (do_output, (options, (verbose, (browser_info,
-          (document_files, (parent_name, (chapter, (name, theories))))))))) =
+          (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
         File.read (Path.explode args_file) |> YXML.parse_body |>
           let open XML.Decode in
             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
-              (pair (list (pair string string)) (pair string (pair string (pair string
-                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
+              (pair (list (pair string string)) (pair string (pair string (pair string (pair string
+                ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
           end;
 
       val _ = Options.set_default options;
@@ -144,6 +144,7 @@
           (Options.string options "document_output")
           (Present.document_variants (Options.string options "document_variants"))
           (map (apply2 Path.explode) document_files)
+          (Path.explode graph_file)
           parent_name (chapter, name)
           verbose;
 
diff -r d57e275b2d82 -r 2c27c3d1fd3b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Jan 25 20:22:20 2015 +0100
+++ b/src/Pure/Tools/build.scala	Sun Jan 25 21:46:21 2015 +0100
@@ -535,13 +535,17 @@
   /* jobs */
 
   private class Job(progress: Progress,
-    name: String, val info: Session_Info, output: Path, do_output: Boolean,
-    verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
+    name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean,
+    browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
   {
     def output_path: Option[Path] = if (do_output) Some(output) else None
 
     private val parent = info.parent.getOrElse("")
 
+    private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
+    try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
+    catch { case ERROR(_) => /*error should be exposed in ML*/ }
+
     private val args_file = Isabelle_System.tmp_file("args")
     File.write(args_file, YXML.string_of_body(
       if (is_pure(name)) Options.encode(info.options)
@@ -550,10 +554,11 @@
           val theories = info.theories.map(x => (x._2, x._3))
           import XML.Encode._
               pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
-                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
-                  list(pair(Options.encode, list(Path.encode))))))))))))(
+                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
+                pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
               (command_timings, (do_output, (info.options, (verbose, (browser_info,
-                (info.document_files, (parent, (info.chapter, (name, theories))))))))))
+                (info.document_files, (Isabelle_System.posix_path(graph_file), (parent,
+                (info.chapter, (name, theories)))))))))))
         }))
 
     private val env =
@@ -623,6 +628,7 @@
     {
       val res = result.join
 
+      graph_file.delete
       args_file.delete
       timeout_request.foreach(_.cancel)
 
@@ -907,7 +913,7 @@
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
                     new Job(progress, name, info, output, do_output, verbose, browser_info,
-                      queue.command_timings(name))
+                      deps(name).session_graph, queue.command_timings(name))
                   loop(pending, running + (name -> (parent_result.heap, job)), results)
                 }
                 else {