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