--- 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;