# HG changeset patch # User wenzelm # Date 939390610 -7200 # Node ID fba7a36e8556ae4bd8446623add277489ed1fa5f # Parent 535112d1f316b47029f1ebb96aa7a7bfeda6b303 isatool_document; diff -r 535112d1f316 -r fba7a36e8556 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Oct 08 15:39:52 1999 +0200 +++ b/src/Pure/Thy/present.ML Fri Oct 08 15:50:10 1999 +0200 @@ -214,13 +214,13 @@ type session_info = {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, - doc_prefix: Path.T option, graph_path: Path.T, all_graph_path: Path.T, + doc_format: string, doc_prefix: Path.T 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_prefix, +fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefix, graph_path, all_graph_path, remote_path) = - {name = name, parent = parent, session = session, path = path, - html_prefix = html_prefix, doc_prefix = doc_prefix, graph_path = graph_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, all_graph_path = all_graph_path, remote_path = remote_path}: session_info; @@ -316,7 +316,7 @@ 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_prefix, graph_path, all_graph_path, remote_path)); + html_prefix, doc, doc_prefix, graph_path, all_graph_path, remote_path)); browser_info := initial_browser_info remote_path all_graph_path path; add_html_index index_text end; @@ -324,18 +324,23 @@ (* finish session *) +fun isatool_document doc_format doc_prefix = + let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'" + in writeln cmd; writeln (execute cmd) end; + fun finish () = with_session () - (fn {name, html_prefix, doc_prefix, graph_path, all_graph_path, path, ...} => + (fn {name, html_prefix, doc_format, doc_prefix, 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}) = - (apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source) doc_prefix; + (doc_prefix |> apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source); 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; - apsome (fn p => Buffer.write (Path.append p doc_index_path) tex_index) doc_prefix; + doc_prefix |> apsome (fn p => + (Buffer.write (Path.append p doc_index_path) tex_index; isatool_document doc_format p)); put_graph graph graph_path; put_graph all_graph all_graph_path; create_index html_prefix;