# HG changeset patch # User wenzelm # Date 1003602217 -7200 # Node ID a35af478aee4eb6e03af9270f2ab04751c272eca # Parent bdae1f29f35dacc1d60c87e378ccfd9a31ca662f graceful interpretation of -i/-d/-D options; verbose: additional messages/warnings; include document graph; diff -r bdae1f29f35d -r a35af478aee4 src/Pure/Thy/present.ML --- 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));