src/Pure/Thy/present.ML
changeset 56533 cd8b6d849b6a
parent 56531 ec4cd116844b
child 56612 74851ff86180
     1.1 --- a/src/Pure/Thy/present.ML	Fri Apr 11 09:36:38 2014 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Apr 11 11:52:28 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val session_name: theory -> string
     1.5    val read_variant: string -> string * string
     1.6    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     1.7 -    string * string -> bool -> theory list -> unit  (*not thread-safe!*)
     1.8 +    (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
     1.9    val finish: unit -> unit  (*not thread-safe!*)
    1.10    val theory_output: string -> string -> unit
    1.11    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    1.12 @@ -170,15 +170,15 @@
    1.13  type session_info =
    1.14    {name: string, chapter: string, info_path: Path.T, info: bool,
    1.15      doc_format: string, doc_graph: bool, doc_output: Path.T option,
    1.16 -    documents: (string * string) list, verbose: bool,
    1.17 -    readme: Path.T option};
    1.18 +    doc_files: (Path.T * Path.T) list, documents: (string * string) list,
    1.19 +    verbose: bool, readme: Path.T option};
    1.20  
    1.21  fun make_session_info
    1.22    (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
    1.23 -    documents, verbose, readme) =
    1.24 +    doc_files, documents, verbose, readme) =
    1.25    {name = name, chapter = chapter, info_path = info_path, info = info,
    1.26      doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    1.27 -    documents = documents, verbose = verbose,
    1.28 +    doc_files = doc_files, documents = documents, verbose = verbose,
    1.29      readme = readme}: session_info;
    1.30  
    1.31  
    1.32 @@ -203,7 +203,7 @@
    1.33  
    1.34  (* init session *)
    1.35  
    1.36 -fun init build info info_path doc doc_graph document_output doc_variants
    1.37 +fun init build info info_path doc doc_graph document_output doc_variants doc_files
    1.38      (chapter, name) verbose thys =
    1.39    if not build andalso not info andalso doc = "" then
    1.40      (browser_info := empty_browser_info; session_info := NONE)
    1.41 @@ -214,7 +214,7 @@
    1.42  
    1.43        val documents =
    1.44          if doc = "" then []
    1.45 -        else if not (can File.check_dir document_path) then
    1.46 +        else if null doc_files andalso not (can File.check_dir document_path) then
    1.47            (if verbose then Output.physical_stderr "Warning: missing document directory\n"
    1.48             else (); [])
    1.49          else doc_variants;
    1.50 @@ -227,7 +227,7 @@
    1.51      in
    1.52        session_info :=
    1.53          SOME (make_session_info (name, chapter, info_path, info, doc,
    1.54 -          doc_graph, doc_output, documents, verbose, readme));
    1.55 +          doc_graph, doc_output, doc_files, documents, verbose, readme));
    1.56        browser_info := init_browser_info (chapter, name) thys;
    1.57        add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
    1.58      end;
    1.59 @@ -275,10 +275,9 @@
    1.60  fun write_tex_index tex_index path =
    1.61    write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
    1.62  
    1.63 -
    1.64  fun finish () =
    1.65 -  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
    1.66 -    documents, verbose, readme, ...} =>
    1.67 +  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
    1.68 +    doc_output, doc_files, documents, verbose, readme, ...} =>
    1.69    let
    1.70      val {theories, tex_index, html_index, graph} = ! browser_info;
    1.71      val thys = Symtab.dest theories;
    1.72 @@ -300,33 +299,30 @@
    1.73         (Isabelle_System.mkdirs session_prefix;
    1.74          File.write_buffer (Path.append session_prefix index_path)
    1.75            (index_buffer html_index |> Buffer.add HTML.end_document);
    1.76 -        (case readme of NONE => () | SOME path => File.copy path session_prefix);
    1.77 +        (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
    1.78          Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
    1.79          Isabelle_System.isabelle_tool "browser" "-b";
    1.80 -        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
    1.81 +        Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
    1.82          List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
    1.83            (HTML.applet_pages name (Url.File index_path, name));
    1.84 -        File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
    1.85 +        Isabelle_System.copy_file (Path.explode "~~/etc/isabelle.css") session_prefix;
    1.86          List.app finish_html thys;
    1.87          if verbose
    1.88          then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
    1.89          else ())
    1.90        else ();
    1.91  
    1.92 -    fun document_job doc_prefix backdrop (name, tags) =
    1.93 +    fun document_job doc_prefix backdrop (doc_name, tags) =
    1.94        let
    1.95 -        val _ =
    1.96 -          File.eq (document_path, doc_prefix) andalso
    1.97 -            error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
    1.98 -        val doc_dir = Path.append doc_prefix (Path.basic name);
    1.99 +        val doc_dir = Path.append doc_prefix (Path.basic doc_name);
   1.100          val _ = Isabelle_System.mkdirs doc_dir;
   1.101          val _ =
   1.102 -          if File.eq (document_path, doc_dir) then ()
   1.103 -          else Isabelle_System.copy_dir document_path doc_dir;
   1.104 -        val _ =
   1.105            Isabelle_System.isabelle_tool "latex"
   1.106              ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
   1.107          val _ =
   1.108 +          if null doc_files then Isabelle_System.copy_dir document_path doc_dir
   1.109 +          else List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
   1.110 +        val _ =
   1.111            (case opt_graphs of
   1.112              NONE => ()
   1.113            | SOME (pdf, eps) =>
   1.114 @@ -338,7 +334,7 @@
   1.115              write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
   1.116        in
   1.117          fn () =>
   1.118 -          (isabelle_document {verbose = true, purge = backdrop} doc_format name tags doc_dir,
   1.119 +          (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
   1.120              fn doc =>
   1.121                if verbose orelse not backdrop then
   1.122                  Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
   1.123 @@ -353,6 +349,12 @@
   1.124          NONE => []
   1.125        | SOME path => map (document_job path false) documents);
   1.126  
   1.127 +    val _ =
   1.128 +      if not (null jobs) andalso null doc_files then
   1.129 +        Output.physical_stderr ("### Document preparation for session " ^ quote name ^
   1.130 +          " without 'document_files'\n")
   1.131 +      else ();
   1.132 +
   1.133      val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>);
   1.134    in
   1.135      browser_info := empty_browser_info;
   1.136 @@ -416,7 +418,7 @@
   1.137      val doc_path = Path.append dir document_path;
   1.138      val _ = Isabelle_System.mkdirs doc_path;
   1.139      val root_path = Path.append doc_path (Path.basic "root.tex");
   1.140 -    val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
   1.141 +    val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
   1.142      val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
   1.143      val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
   1.144  
   1.145 @@ -438,7 +440,7 @@
   1.146      val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
   1.147      val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
   1.148      val _ = Isabelle_System.mkdirs target_dir;
   1.149 -    val _ = File.copy result target;
   1.150 +    val _ = Isabelle_System.copy_file result target;
   1.151    in
   1.152      Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &")
   1.153    end);