src/Pure/Thy/present.ML
changeset 59445 2c27c3d1fd3b
parent 59244 19b5fc4b2b38
child 59446 4427f04fca57
     1.1 --- a/src/Pure/Thy/present.ML	Sun Jan 25 20:22:20 2015 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Jan 25 21:46:21 2015 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4    val document_enabled: string -> bool
     1.5    val document_variants: string -> (string * string) list
     1.6    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     1.7 -    (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
     1.8 -  val finish: unit -> unit  (*not thread-safe!*)
     1.9 +    (Path.T * Path.T) list -> Path.T -> string * string -> bool -> theory list -> unit
    1.10 +  val finish: unit -> unit
    1.11    val theory_output: string -> string -> unit
    1.12    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    1.13    val display_drafts: Path.T list -> int
    1.14 @@ -34,7 +34,6 @@
    1.15  val doc_indexN = "session";
    1.16  val graph_path = Path.basic "session.graph";
    1.17  val graph_pdf_path = Path.basic "session_graph.pdf";
    1.18 -val graph_eps_path = Path.basic "session_graph.eps";
    1.19  
    1.20  fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
    1.21  
    1.22 @@ -163,16 +162,16 @@
    1.23  type session_info =
    1.24    {name: string, chapter: string, info_path: Path.T, info: bool,
    1.25      doc_format: string, doc_graph: bool, doc_output: Path.T option,
    1.26 -    doc_files: (Path.T * Path.T) list, documents: (string * string) list,
    1.27 +    doc_files: (Path.T * Path.T) list, graph_file: Path.T, documents: (string * string) list,
    1.28      verbose: bool, readme: Path.T option};
    1.29  
    1.30  fun make_session_info
    1.31    (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
    1.32 -    doc_files, documents, verbose, readme) =
    1.33 +    doc_files, graph_file, documents, verbose, readme) =
    1.34    {name = name, chapter = chapter, info_path = info_path, info = info,
    1.35      doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    1.36 -    doc_files = doc_files, documents = documents, verbose = verbose,
    1.37 -    readme = readme}: session_info;
    1.38 +    doc_files = doc_files, graph_file = graph_file, documents = documents,
    1.39 +    verbose = verbose, readme = readme}: session_info;
    1.40  
    1.41  
    1.42  (* state *)
    1.43 @@ -206,7 +205,7 @@
    1.44  
    1.45  (* init session *)
    1.46  
    1.47 -fun init build info info_path doc doc_graph document_output doc_variants doc_files
    1.48 +fun init build info info_path doc doc_graph document_output doc_variants doc_files graph_file
    1.49      (chapter, name) verbose thys =
    1.50    if not build andalso not info andalso doc = "" then
    1.51      (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
    1.52 @@ -230,7 +229,7 @@
    1.53      in
    1.54        session_info :=
    1.55          SOME (make_session_info (name, chapter, info_path, info, doc,
    1.56 -          doc_graph, doc_output, doc_files, documents, verbose, readme));
    1.57 +          doc_graph, doc_output, doc_files, graph_file, documents, verbose, readme));
    1.58        Synchronized.change browser_info (K (init_browser_info (chapter, name) thys));
    1.59        add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
    1.60      end;
    1.61 @@ -252,20 +251,6 @@
    1.62        else ();
    1.63    in doc_path end;
    1.64  
    1.65 -fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir =>
    1.66 -  let
    1.67 -    val pdf_path = Path.append dir graph_pdf_path;
    1.68 -    val eps_path = Path.append dir graph_eps_path;
    1.69 -    val graph_path = Path.append dir graph_path;
    1.70 -    val _ = Graph_Display.write_graph_browser graph_path graph;
    1.71 -    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
    1.72 -  in
    1.73 -    if Isabelle_System.isabelle_tool "browser" args = 0 andalso
    1.74 -      File.exists pdf_path andalso File.exists eps_path
    1.75 -    then (File.read pdf_path, File.read eps_path)
    1.76 -    else error "Failed to prepare dependency graph"
    1.77 -  end);
    1.78 -
    1.79  
    1.80  (* finish session -- output all generated text *)
    1.81  
    1.82 @@ -280,10 +265,11 @@
    1.83  
    1.84  fun finish () =
    1.85    with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
    1.86 -    doc_output, doc_files, documents, verbose, readme, ...} =>
    1.87 +    doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
    1.88    let
    1.89      val {theories, tex_index, html_index, graph} = Synchronized.value browser_info;
    1.90      val thys = Symtab.dest theories;
    1.91 +    val sorted_graph = Graph_Display.sort_graph graph;
    1.92  
    1.93      val chapter_prefix = Path.append info_path (Path.basic chapter);
    1.94      val session_prefix = Path.append chapter_prefix (Path.basic name);
    1.95 @@ -291,12 +277,6 @@
    1.96      fun finish_html (a, {html_source, ...}: theory_info) =
    1.97        File.write (Path.append session_prefix (html_path a)) html_source;
    1.98  
    1.99 -    val sorted_graph = Graph_Display.sort_graph graph;
   1.100 -    val opt_graphs =
   1.101 -      if doc_graph andalso not (null documents) then
   1.102 -        SOME (isabelle_browser sorted_graph)
   1.103 -      else NONE;
   1.104 -
   1.105      val _ =
   1.106        if info then
   1.107         (Isabelle_System.mkdirs session_prefix;
   1.108 @@ -323,12 +303,7 @@
   1.109            Isabelle_System.isabelle_tool "latex"
   1.110              ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
   1.111          val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
   1.112 -        val _ =
   1.113 -          (case opt_graphs of
   1.114 -            NONE => ()
   1.115 -          | SOME (pdf, eps) =>
   1.116 -              (File.write (Path.append doc_dir graph_pdf_path) pdf;
   1.117 -                File.write (Path.append doc_dir graph_eps_path) eps));
   1.118 +        val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir graph_pdf_path);
   1.119          val _ = write_tex_index tex_index doc_dir;
   1.120          val _ =
   1.121            List.app (fn (a, {tex_source, ...}) =>