--- a/src/Pure/Thy/present.ML Sat Oct 20 20:22:17 2001 +0200
+++ b/src/Pure/Thy/present.ML Sat Oct 20 20:23:37 2001 +0200
@@ -17,7 +17,7 @@
include BASIC_PRESENT
val write_graph: {name: string, ID: string, dir: string, unfold: bool,
path: string, parents: string list} list -> Path.T -> unit
- val init: bool -> string -> string list -> string -> Path.T option
+ val init: bool -> string -> bool -> string list -> string -> Path.T option
-> Url.T option * bool -> bool -> unit
val finish: unit -> unit
val init_theory: string -> unit
@@ -48,10 +48,14 @@
val tex_path = tex_ext o Path.basic;
val html_ext = Path.ext "html";
val html_path = html_ext o Path.basic;
-val graph_path = Path.ext "graph" o Path.basic;
val index_path = Path.basic "index.html";
+val readme_html_path = Path.basic "README.html";
+val readme_path = Path.basic "README";
val doc_path = Path.basic "document";
val doc_indexN = "session";
+val graph_path = Path.basic "session.graph";
+val graph_pdf_path = Path.basic "session_graph.pdf";
+val graph_eps_path = Path.basic "session_graph.eps";
val session_path = Path.basic ".session";
val session_entries_path = Path.unpack ".session/entries";
@@ -62,6 +66,8 @@
| mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
+fun show_path path = Path.pack (Path.append (File.pwd ()) path);
+
(** additional theory data **)
@@ -138,20 +144,20 @@
(* type browser_info *)
-type browser_info = {theories: theory_info Symtab.table, tex_index: Buffer.T,
- html_index: Buffer.T, graph: graph_node list};
+type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
+ tex_index: Buffer.T, html_index: Buffer.T, graph: graph_node list};
-fun make_browser_info (theories, tex_index, html_index, graph) =
- {theories = theories, tex_index = tex_index, html_index = html_index,
+fun make_browser_info (theories, files, tex_index, html_index, graph) =
+ {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
graph = graph}: browser_info;
-val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, Buffer.empty, []);
+val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []);
fun init_browser_info remote_path curr_sess = make_browser_info
- (Symtab.empty, Buffer.empty, Buffer.empty, init_graph remote_path curr_sess);
+ (Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess);
-fun map_browser_info f {theories, tex_index, html_index, graph} =
- make_browser_info (f (theories, tex_index, html_index, graph));
+fun map_browser_info f {theories, files, tex_index, html_index, graph} =
+ make_browser_info (f (theories, files, tex_index, html_index, graph));
(* state *)
@@ -163,28 +169,32 @@
fun no_document f x = Library.setmp suppress_tex_source true f x;
fun init_theory_info name info =
- change_browser_info (fn (theories, tex_index, html_index, graph) =>
- (Symtab.update ((name, info), theories), tex_index, html_index, graph));
+ change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
+ (Symtab.update ((name, info), theories), files, tex_index, html_index, graph));
fun change_theory_info name f =
- change_browser_info (fn (info as (theories, tex_index, html_index, graph)) =>
+ change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
(case Symtab.lookup (theories, name) of
None => (warning ("Browser info: cannot access theory document " ^ quote name); info)
- | Some info => (Symtab.update ((name, map_theory_info f info), theories),
+ | Some info => (Symtab.update ((name, map_theory_info f info), theories), files,
tex_index, html_index, graph)));
+fun add_file file =
+ change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
+ (theories, file :: files, tex_index, html_index, graph));
+
fun add_tex_index txt =
- change_browser_info (fn (theories, tex_index, html_index, graph) =>
- (theories, Buffer.add txt tex_index, html_index, graph));
+ change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
+ (theories, files, Buffer.add txt tex_index, html_index, graph));
fun add_html_index txt =
- change_browser_info (fn (theories, tex_index, html_index, graph) =>
- (theories, tex_index, Buffer.add txt html_index, graph));
+ change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
+ (theories, files, tex_index, Buffer.add txt html_index, graph));
fun add_graph_entry e =
- change_browser_info (fn (theories, tex_index, html_index, graph) =>
- (theories, tex_index, html_index, ins_graph_entry e graph));
+ change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
+ (theories, files, tex_index, html_index, ins_graph_entry e graph));
fun add_tex_source name txt =
if ! suppress_tex_source then ()
@@ -205,14 +215,16 @@
type session_info =
{name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
- doc_format: string, doc_prefixes: (Path.T * Path.T option) option,
- remote_path: Url.T option, verbose: bool};
+ info: bool, doc_format: string, doc_graph: bool, doc_prefix1: Path.T option,
+ doc_prefix2: Path.T option, remote_path: Url.T option, verbose: bool, readme: Path.T option};
fun make_session_info
- (name, parent, session, path, html_prefix, doc_format, doc_prefixes, remote_path, verbose) =
+ (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_prefix1,
+ doc_prefix2, remote_path, verbose, readme) =
{name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
- doc_format = doc_format, doc_prefixes = doc_prefixes, remote_path = remote_path,
- verbose = verbose}: session_info;
+ info = info, doc_format = doc_format, doc_graph = doc_graph, doc_prefix1 = doc_prefix1,
+ doc_prefix2 = doc_prefix2, remote_path = remote_path, verbose = verbose,
+ readme = readme}: session_info;
(* state *)
@@ -254,103 +266,132 @@
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
-fun could_copy inpath outpath =
- if File.exists inpath then (File.copy inpath outpath; true)
- else false;
-
fun copy_files path1 path2 =
(File.mkdir path2;
File.system_command (*FIXME: quote paths!?*)
("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
-fun init false _ _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
- | init true doc path name dump_path (remote_path, first_time) verbose =
- let
- val parent_name = name_of_session (Library.take (length path - 1, path));
- val session_name = name_of_session path;
- val sess_prefix = Path.make path;
-
- val out_path = Path.expand output_path;
- val html_prefix = Path.append out_path sess_prefix;
+fun init info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
+ if not info andalso doc = "" andalso is_none doc_prefix2 then
+ (browser_info := empty_browser_info; session_info := None)
+ else
+ let
+ val parent_name = name_of_session (Library.take (length path - 1, path));
+ val session_name = name_of_session path;
+ val sess_prefix = Path.make path;
+ val html_prefix = Path.append (Path.expand output_path) sess_prefix;
- val (doc_prefixes, document_path) =
- if doc = "" then (None, None)
- else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
-
- val graph_up_lnk = (Url.file index_path, session_name);
-
- val _ =
- (copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class")
- (Path.append html_prefix (Path.basic "awtUtilities"));
- copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class")
- (Path.append html_prefix (Path.basic "GraphBrowser")));
+ val (doc_prefix1, document_path) =
+ if doc = "" then (None, None)
+ else if not (File.exists doc_path) then (conditional verbose (fn () =>
+ std_error "Warning: missing document directory\n"); (None, None))
+ else (Some (Path.append html_prefix doc_path), Some (Path.ext doc doc_path));
- fun prep_readme readme =
- let val readme_path = Path.basic readme in
- if could_copy readme_path (Path.append html_prefix readme_path) then Some readme_path
- else None
- end;
- val opt_readme =
- (case prep_readme "README.html" of None => prep_readme "README" | some => some);
-
- val parent_index_path = Path.append Path.parent index_path;
- val index_up_lnk = if first_time then
- Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path))
- else Url.file parent_index_path;
+ val parent_index_path = Path.append Path.parent index_path;
+ val index_up_lnk = if first_time then
+ Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path))
+ else Url.file parent_index_path;
+ val readme =
+ if File.exists readme_html_path then Some readme_html_path
+ else if File.exists readme_path then Some readme_path
+ else None;
- val index_text = HTML.begin_index (index_up_lnk, parent_name)
- (Url.file index_path, session_name) (apsome Url.file opt_readme)
- (apsome Url.file document_path) (Url.unpack "medium.html");
- in
- File.mkdir (Path.append html_prefix session_path);
- File.write (Path.append html_prefix session_entries_path) "";
- if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
- seq (fn (name, txt) => File.write (Path.append html_prefix (Path.basic name)) txt)
- (HTML.applet_pages session_name graph_up_lnk);
- session_info := Some (make_session_info (name, parent_name, session_name, path,
- html_prefix, doc, doc_prefixes, remote_path, verbose));
- browser_info := init_browser_info remote_path path;
- add_html_index index_text
- end;
+ val index_text = HTML.begin_index (index_up_lnk, parent_name)
+ (Url.file index_path, session_name) (apsome Url.file readme)
+ (apsome Url.file document_path) (Url.unpack "medium.html");
+ in
+ session_info := Some (make_session_info (name, parent_name, session_name, path, html_prefix,
+ info, doc, doc_graph, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
+ browser_info := init_browser_info remote_path path;
+ add_html_index index_text
+ end;
-(* finish session *)
+(* finish session -- output all generated text *)
+
+fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
-fun isatool_document verbose doc_format doc_prefix =
- let
- val cmd = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' "
- ^ (if verbose then "-v " else "") ^ File.quote_sysify_path doc_prefix;
- in
- writeln cmd;
- if system cmd <> 0 orelse not (File.exists (Path.ext doc_format doc_prefix)) then
+fun isatool_document doc_format path =
+ let val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^ File.quote_sysify_path path in
+ writeln s;
+ if system s <> 0 orelse not (File.exists (Path.ext doc_format path)) 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 isatool_browser graph =
+ let
+ val pdfpath = File.tmp_path graph_pdf_path;
+ val epspath = File.tmp_path graph_eps_path;
+ val gpath = File.tmp_path graph_path;
+ val s = "\"$ISATOOL\" browser -o " ^ File.quote_sysify_path pdfpath ^ " " ^
+ File.quote_sysify_path gpath;
+ in
+ write_graph graph gpath;
+ if system s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath) then
+ error "Failed to prepare dependency graph"
+ else
+ let val pdf = File.read pdfpath and eps = File.read epspath
+ in File.rm pdfpath; File.rm epspath; File.rm gpath; (pdf, eps) end
+ end;
-
-fun finish () = with_session ()
- (fn {name, html_prefix, doc_format, doc_prefixes, path, verbose, ...} =>
+fun finish () = with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
+ doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
let
- val {theories, tex_index, html_index, graph} = ! browser_info;
+ val {theories, files, tex_index, html_index, graph} = ! browser_info;
+ val thys = Symtab.dest theories;
val parent_html_prefix = Path.append html_prefix Path.parent;
- fun finish_node (a, {tex_source, html_source = _, html}) =
- (doc_prefixes |> apsome (write_texes tex_source a);
- Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
+ fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
+ fun finish_html (a, {html, ...}: theory_info) =
+ Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html);
+
+ val opt_graphs =
+ if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
+ Some (isatool_browser graph)
+ else None;
+
+ fun doc_common path =
+ ((case opt_graphs of None => () | Some (pdf, eps) =>
+ (File.write (Path.append path graph_pdf_path) pdf;
+ File.write (Path.append path graph_eps_path) eps));
+ write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
+ seq (finish_tex path) thys);
in
- seq finish_node (Symtab.dest theories);
- Buffer.write (Path.append html_prefix pre_index_path) html_index;
- doc_prefixes |> apsome (write_texes (Buffer.add Latex.tex_trailer tex_index) doc_indexN);
- doc_prefixes |> apsome (isatool_document verbose doc_format o #1);
- write_graph graph (Path.append html_prefix (graph_path "session"));
- create_index html_prefix;
- if length path > 1 then update_index parent_html_prefix name else ();
+ conditional info (fn () =>
+ (File.mkdir (Path.append html_prefix session_path);
+ Buffer.write (Path.append html_prefix pre_index_path) html_index;
+ File.write (Path.append html_prefix session_entries_path) "";
+ create_index html_prefix;
+ if length path > 1 then update_index parent_html_prefix name else ();
+ (case readme of None => () | Some path => File.copy path (Path.append html_prefix path));
+ write_graph graph (Path.append html_prefix graph_path);
+ copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class")
+ (Path.append html_prefix (Path.basic "awtUtilities"));
+ copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class")
+ (Path.append html_prefix (Path.basic "GraphBrowser"));
+ seq (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
+ (HTML.applet_pages name (Url.file index_path, name));
+ seq finish_html thys;
+ seq (uncurry File.write) files;
+ conditional verbose (fn () =>
+ std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));
+
+ (case doc_prefix1 of None => () | Some path =>
+ (File.mkdir html_prefix;
+ File.copy_all doc_path html_prefix;
+ doc_common path;
+ isatool_document doc_format path;
+ conditional verbose (fn () =>
+ std_error ("Document at " ^ show_path (Path.ext doc_format path) ^ "\n"))));
+
+ (case doc_prefix2 of None => () | Some path =>
+ (File.mkdir path;
+ copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
+ doc_common path;
+ conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
+
browser_info := empty_browser_info;
session_info := None
end);
@@ -395,8 +436,8 @@
val base = Path.base path;
val base_html = html_ext base;
in
- File.write (Path.append html_prefix base_html)
- (HTML.ml_file (Url.file base) (File.read path));
+ add_file (Path.append html_prefix base_html,
+ HTML.ml_file (Url.file base) (File.read path));
(Some (Url.file base_html), Url.file raw_path, loadit)
end
| None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));