provide session_graph.pdf via Isabelle/Scala;
authorwenzelm
Sun Jan 25 21:46:21 2015 +0100 (2015-01-25)
changeset 594452c27c3d1fd3b
parent 59444 d57e275b2d82
child 59446 4427f04fca57
provide session_graph.pdf via Isabelle/Scala;
src/Pure/PIDE/session.ML
src/Pure/Thy/present.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/session.ML	Sun Jan 25 20:22:20 2015 +0100
     1.2 +++ b/src/Pure/PIDE/session.ML	Sun Jan 25 21:46:21 2015 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    val welcome: unit -> string
     1.5    val get_keywords: unit -> Keyword.keywords
     1.6    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     1.7 -    (Path.T * Path.T) list -> string -> string * string -> bool -> unit
     1.8 +    (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
     1.9    val shutdown: unit -> unit
    1.10    val finish: unit -> unit
    1.11    val save: string -> unit
    1.12 @@ -42,7 +42,7 @@
    1.13  
    1.14  (* init *)
    1.15  
    1.16 -fun init build info info_path doc doc_graph doc_output doc_variants doc_files
    1.17 +fun init build info info_path doc doc_graph doc_output doc_variants doc_files graph_file
    1.18      parent (chapter, name) verbose =
    1.19    if #name (! session) <> parent orelse not (! session_finished) then
    1.20      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    1.21 @@ -52,7 +52,7 @@
    1.22        val _ = session_finished := false;
    1.23      in
    1.24        Present.init build info info_path (if doc = "false" then "" else doc)
    1.25 -        doc_graph doc_output doc_variants doc_files (chapter, name)
    1.26 +        doc_graph doc_output doc_variants doc_files graph_file (chapter, name)
    1.27          verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    1.28      end;
    1.29  
     2.1 --- a/src/Pure/Thy/present.ML	Sun Jan 25 20:22:20 2015 +0100
     2.2 +++ b/src/Pure/Thy/present.ML	Sun Jan 25 21:46:21 2015 +0100
     2.3 @@ -10,8 +10,8 @@
     2.4    val document_enabled: string -> bool
     2.5    val document_variants: string -> (string * string) list
     2.6    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     2.7 -    (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
     2.8 -  val finish: unit -> unit  (*not thread-safe!*)
     2.9 +    (Path.T * Path.T) list -> Path.T -> string * string -> bool -> theory list -> unit
    2.10 +  val finish: unit -> unit
    2.11    val theory_output: string -> string -> unit
    2.12    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    2.13    val display_drafts: Path.T list -> int
    2.14 @@ -34,7 +34,6 @@
    2.15  val doc_indexN = "session";
    2.16  val graph_path = Path.basic "session.graph";
    2.17  val graph_pdf_path = Path.basic "session_graph.pdf";
    2.18 -val graph_eps_path = Path.basic "session_graph.eps";
    2.19  
    2.20  fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
    2.21  
    2.22 @@ -163,16 +162,16 @@
    2.23  type session_info =
    2.24    {name: string, chapter: string, info_path: Path.T, info: bool,
    2.25      doc_format: string, doc_graph: bool, doc_output: Path.T option,
    2.26 -    doc_files: (Path.T * Path.T) list, documents: (string * string) list,
    2.27 +    doc_files: (Path.T * Path.T) list, graph_file: Path.T, documents: (string * string) list,
    2.28      verbose: bool, readme: Path.T option};
    2.29  
    2.30  fun make_session_info
    2.31    (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
    2.32 -    doc_files, documents, verbose, readme) =
    2.33 +    doc_files, graph_file, documents, verbose, readme) =
    2.34    {name = name, chapter = chapter, info_path = info_path, info = info,
    2.35      doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    2.36 -    doc_files = doc_files, documents = documents, verbose = verbose,
    2.37 -    readme = readme}: session_info;
    2.38 +    doc_files = doc_files, graph_file = graph_file, documents = documents,
    2.39 +    verbose = verbose, readme = readme}: session_info;
    2.40  
    2.41  
    2.42  (* state *)
    2.43 @@ -206,7 +205,7 @@
    2.44  
    2.45  (* init session *)
    2.46  
    2.47 -fun init build info info_path doc doc_graph document_output doc_variants doc_files
    2.48 +fun init build info info_path doc doc_graph document_output doc_variants doc_files graph_file
    2.49      (chapter, name) verbose thys =
    2.50    if not build andalso not info andalso doc = "" then
    2.51      (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
    2.52 @@ -230,7 +229,7 @@
    2.53      in
    2.54        session_info :=
    2.55          SOME (make_session_info (name, chapter, info_path, info, doc,
    2.56 -          doc_graph, doc_output, doc_files, documents, verbose, readme));
    2.57 +          doc_graph, doc_output, doc_files, graph_file, documents, verbose, readme));
    2.58        Synchronized.change browser_info (K (init_browser_info (chapter, name) thys));
    2.59        add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
    2.60      end;
    2.61 @@ -252,20 +251,6 @@
    2.62        else ();
    2.63    in doc_path end;
    2.64  
    2.65 -fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir =>
    2.66 -  let
    2.67 -    val pdf_path = Path.append dir graph_pdf_path;
    2.68 -    val eps_path = Path.append dir graph_eps_path;
    2.69 -    val graph_path = Path.append dir graph_path;
    2.70 -    val _ = Graph_Display.write_graph_browser graph_path graph;
    2.71 -    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
    2.72 -  in
    2.73 -    if Isabelle_System.isabelle_tool "browser" args = 0 andalso
    2.74 -      File.exists pdf_path andalso File.exists eps_path
    2.75 -    then (File.read pdf_path, File.read eps_path)
    2.76 -    else error "Failed to prepare dependency graph"
    2.77 -  end);
    2.78 -
    2.79  
    2.80  (* finish session -- output all generated text *)
    2.81  
    2.82 @@ -280,10 +265,11 @@
    2.83  
    2.84  fun finish () =
    2.85    with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
    2.86 -    doc_output, doc_files, documents, verbose, readme, ...} =>
    2.87 +    doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
    2.88    let
    2.89      val {theories, tex_index, html_index, graph} = Synchronized.value browser_info;
    2.90      val thys = Symtab.dest theories;
    2.91 +    val sorted_graph = Graph_Display.sort_graph graph;
    2.92  
    2.93      val chapter_prefix = Path.append info_path (Path.basic chapter);
    2.94      val session_prefix = Path.append chapter_prefix (Path.basic name);
    2.95 @@ -291,12 +277,6 @@
    2.96      fun finish_html (a, {html_source, ...}: theory_info) =
    2.97        File.write (Path.append session_prefix (html_path a)) html_source;
    2.98  
    2.99 -    val sorted_graph = Graph_Display.sort_graph graph;
   2.100 -    val opt_graphs =
   2.101 -      if doc_graph andalso not (null documents) then
   2.102 -        SOME (isabelle_browser sorted_graph)
   2.103 -      else NONE;
   2.104 -
   2.105      val _ =
   2.106        if info then
   2.107         (Isabelle_System.mkdirs session_prefix;
   2.108 @@ -323,12 +303,7 @@
   2.109            Isabelle_System.isabelle_tool "latex"
   2.110              ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
   2.111          val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
   2.112 -        val _ =
   2.113 -          (case opt_graphs of
   2.114 -            NONE => ()
   2.115 -          | SOME (pdf, eps) =>
   2.116 -              (File.write (Path.append doc_dir graph_pdf_path) pdf;
   2.117 -                File.write (Path.append doc_dir graph_eps_path) eps));
   2.118 +        val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir graph_pdf_path);
   2.119          val _ = write_tex_index tex_index doc_dir;
   2.120          val _ =
   2.121            List.app (fn (a, {tex_source, ...}) =>
     3.1 --- a/src/Pure/Tools/build.ML	Sun Jan 25 20:22:20 2015 +0100
     3.2 +++ b/src/Pure/Tools/build.ML	Sun Jan 25 21:46:21 2015 +0100
     3.3 @@ -124,12 +124,12 @@
     3.4        val _ = SHA1_Samples.test ();
     3.5  
     3.6        val (command_timings, (do_output, (options, (verbose, (browser_info,
     3.7 -          (document_files, (parent_name, (chapter, (name, theories))))))))) =
     3.8 +          (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
     3.9          File.read (Path.explode args_file) |> YXML.parse_body |>
    3.10            let open XML.Decode in
    3.11              pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    3.12 -              (pair (list (pair string string)) (pair string (pair string (pair string
    3.13 -                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
    3.14 +              (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    3.15 +                ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
    3.16            end;
    3.17  
    3.18        val _ = Options.set_default options;
    3.19 @@ -144,6 +144,7 @@
    3.20            (Options.string options "document_output")
    3.21            (Present.document_variants (Options.string options "document_variants"))
    3.22            (map (apply2 Path.explode) document_files)
    3.23 +          (Path.explode graph_file)
    3.24            parent_name (chapter, name)
    3.25            verbose;
    3.26  
     4.1 --- a/src/Pure/Tools/build.scala	Sun Jan 25 20:22:20 2015 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Sun Jan 25 21:46:21 2015 +0100
     4.3 @@ -535,13 +535,17 @@
     4.4    /* jobs */
     4.5  
     4.6    private class Job(progress: Progress,
     4.7 -    name: String, val info: Session_Info, output: Path, do_output: Boolean,
     4.8 -    verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
     4.9 +    name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean,
    4.10 +    browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
    4.11    {
    4.12      def output_path: Option[Path] = if (do_output) Some(output) else None
    4.13  
    4.14      private val parent = info.parent.getOrElse("")
    4.15  
    4.16 +    private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
    4.17 +    try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
    4.18 +    catch { case ERROR(_) => /*error should be exposed in ML*/ }
    4.19 +
    4.20      private val args_file = Isabelle_System.tmp_file("args")
    4.21      File.write(args_file, YXML.string_of_body(
    4.22        if (is_pure(name)) Options.encode(info.options)
    4.23 @@ -550,10 +554,11 @@
    4.24            val theories = info.theories.map(x => (x._2, x._3))
    4.25            import XML.Encode._
    4.26                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
    4.27 -                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
    4.28 -                  list(pair(Options.encode, list(Path.encode))))))))))))(
    4.29 +                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
    4.30 +                pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
    4.31                (command_timings, (do_output, (info.options, (verbose, (browser_info,
    4.32 -                (info.document_files, (parent, (info.chapter, (name, theories))))))))))
    4.33 +                (info.document_files, (Isabelle_System.posix_path(graph_file), (parent,
    4.34 +                (info.chapter, (name, theories)))))))))))
    4.35          }))
    4.36  
    4.37      private val env =
    4.38 @@ -623,6 +628,7 @@
    4.39      {
    4.40        val res = result.join
    4.41  
    4.42 +      graph_file.delete
    4.43        args_file.delete
    4.44        timeout_request.foreach(_.cancel)
    4.45  
    4.46 @@ -907,7 +913,7 @@
    4.47                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    4.48                    val job =
    4.49                      new Job(progress, name, info, output, do_output, verbose, browser_info,
    4.50 -                      queue.command_timings(name))
    4.51 +                      deps(name).session_graph, queue.command_timings(name))
    4.52                    loop(pending, running + (name -> (parent_result.heap, job)), results)
    4.53                  }
    4.54                  else {