src/Pure/Thy/present.ML

--- a/src/Pure/Thy/present.ML	Sat Feb 05 16:54:27 2000 +0100
+++ b/src/Pure/Thy/present.ML	Sat Feb 05 16:57:02 2000 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 
-Theory presentation (HTML, graph files, simple LaTeX documents).
+Theory presentation (HTML, graph files, (PDF)LaTeX documents).
 *)
 
 signature BASIC_PRESENT =
@@ -13,7 +13,7 @@
 signature PRESENT =
 sig
   include BASIC_PRESENT
-  val init: bool -> string -> string list -> string -> Url.T option * bool -> unit
+  val init: bool -> string -> string list -> string -> Path.T option -> Url.T option * bool -> unit
   val finish: unit -> unit
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
@@ -53,7 +53,7 @@
 val graph_path = Path.ext "graph" o Path.basic;
 val index_path = Path.basic "index.html";
 val doc_path = Path.basic "document";
-val doc_index_path = tex_path "session";
+val doc_indexN = "session";
 
 val session_path = Path.basic ".session";
 val session_entries_path = Path.unpack ".session/entries";
@@ -216,13 +216,13 @@
 
 type session_info =
   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
-    doc_format: string, doc_prefix: Path.T option, graph_path: Path.T, all_graph_path: Path.T,
-    remote_path: Url.T option};
+    doc_format: string, doc_prefixes: (Path.T * Path.T option) option, graph_path: Path.T,
+    all_graph_path: Path.T, remote_path: Url.T option};
 
-fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefix,
+fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefixes,
     graph_path, all_graph_path, remote_path) =
   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
-    doc_format = doc_format, doc_prefix = doc_prefix, graph_path = graph_path,
+    doc_format = doc_format, doc_prefixes = doc_prefixes, graph_path = graph_path,
     all_graph_path = all_graph_path, remote_path = remote_path}: session_info;
 
 
@@ -269,8 +269,8 @@
   if File.exists inpath then (File.copy inpath outpath; true)
   else false;
 
-fun init false _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
-  | init true doc path name (remote_path, first_time) =
+fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
+  | init true doc path name dump_path (remote_path, first_time) =
       let
         val parent_name = name_of_session (take (length path - 1, path));
         val session_name = name_of_session path;
@@ -279,9 +279,9 @@
         val out_path = Path.expand output_path;
         val html_prefix = Path.append out_path sess_prefix;
 
-        val (doc_prefix, document_path) =
+        val (doc_prefixes, document_path) =
           if doc = "" then (None, None)
-          else (Some (Path.append html_prefix doc_path), Some (Path.ext doc doc_path));
+          else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
 
         val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix];
         val graph_path = Path.append graph_prefix (Path.basic "session.graph");
@@ -314,11 +314,11 @@
       in
         File.mkdir (Path.append html_prefix session_path);
         File.write (Path.append html_prefix session_entries_path) "";
-        if is_some doc_prefix then File.copy_all doc_path html_prefix else ();
+        if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
         seq (fn (name, txt) => File.write (Path.append graph_prefix (Path.basic name)) txt)
           (HTML.applet_pages session_name codebase graph_up_lnk (length path = 1));
         session_info := Some (make_session_info (name, parent_name, session_name, path,
-          html_prefix, doc, doc_prefix, graph_path, all_graph_path, remote_path));
+          html_prefix, doc, doc_prefixes, graph_path, all_graph_path, remote_path));
         browser_info := initial_browser_info remote_path all_graph_path path;
         add_html_index index_text
       end;
@@ -330,19 +330,25 @@
   let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
   in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
 
+fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
+
+fun write_texes src name (path, None) = write_tex src name path
+  | write_texes src name (path, Some path') = (write_tex src name path; write_tex src name path');
+
+
 fun finish () = with_session ()
-    (fn {name, html_prefix, doc_format, doc_prefix, graph_path, all_graph_path, path, ...} =>
+    (fn {name, html_prefix, doc_format, doc_prefixes, graph_path, all_graph_path, path, ...} =>
   let
     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
 
     fun finish_node (a, {tex_source, html_source = _, html}) =
-     (doc_prefix |> apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source);
+     (doc_prefixes |> apsome (write_texes tex_source a);
       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   in
     seq finish_node (Symtab.dest theories);
     Buffer.write (Path.append html_prefix pre_index_path) html_index;
-    doc_prefix |> apsome (fn p =>
-     (Buffer.write (Path.append p doc_index_path) tex_index; isatool_document doc_format p));
+    doc_prefixes |> apsome (write_texes tex_index doc_indexN);
+    doc_prefixes |> apsome (isatool_document doc_format o #1);
     put_graph graph graph_path;
     put_graph all_graph all_graph_path;
     create_index html_prefix;