src/Pure/Tools/build.scala
changeset 59445 2c27c3d1fd3b
parent 59444 d57e275b2d82
child 59692 03aa1b63af10
     1.1 --- a/src/Pure/Tools/build.scala	Sun Jan 25 20:22:20 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Jan 25 21:46:21 2015 +0100
     1.3 @@ -535,13 +535,17 @@
     1.4    /* jobs */
     1.5  
     1.6    private class Job(progress: Progress,
     1.7 -    name: String, val info: Session_Info, output: Path, do_output: Boolean,
     1.8 -    verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
     1.9 +    name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean,
    1.10 +    browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
    1.11    {
    1.12      def output_path: Option[Path] = if (do_output) Some(output) else None
    1.13  
    1.14      private val parent = info.parent.getOrElse("")
    1.15  
    1.16 +    private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
    1.17 +    try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
    1.18 +    catch { case ERROR(_) => /*error should be exposed in ML*/ }
    1.19 +
    1.20      private val args_file = Isabelle_System.tmp_file("args")
    1.21      File.write(args_file, YXML.string_of_body(
    1.22        if (is_pure(name)) Options.encode(info.options)
    1.23 @@ -550,10 +554,11 @@
    1.24            val theories = info.theories.map(x => (x._2, x._3))
    1.25            import XML.Encode._
    1.26                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
    1.27 -                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
    1.28 -                  list(pair(Options.encode, list(Path.encode))))))))))))(
    1.29 +                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
    1.30 +                pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
    1.31                (command_timings, (do_output, (info.options, (verbose, (browser_info,
    1.32 -                (info.document_files, (parent, (info.chapter, (name, theories))))))))))
    1.33 +                (info.document_files, (Isabelle_System.posix_path(graph_file), (parent,
    1.34 +                (info.chapter, (name, theories)))))))))))
    1.35          }))
    1.36  
    1.37      private val env =
    1.38 @@ -623,6 +628,7 @@
    1.39      {
    1.40        val res = result.join
    1.41  
    1.42 +      graph_file.delete
    1.43        args_file.delete
    1.44        timeout_request.foreach(_.cancel)
    1.45  
    1.46 @@ -907,7 +913,7 @@
    1.47                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.48                    val job =
    1.49                      new Job(progress, name, info, output, do_output, verbose, browser_info,
    1.50 -                      queue.command_timings(name))
    1.51 +                      deps(name).session_graph, queue.command_timings(name))
    1.52                    loop(pending, running + (name -> (parent_result.heap, job)), results)
    1.53                  }
    1.54                  else {