diff -r 7eecd020e367 -r 2142883ec29f src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Mar 20 19:10:09 2011 +0100 +++ b/src/Pure/Thy/present.ML Sun Mar 20 19:34:18 2011 +0100 @@ -215,16 +215,16 @@ type session_info = {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, - doc_prefix1: (Path.T * Path.T) option, dump_prefix: (bool * Path.T) option, - remote_path: Url.T option, verbose: bool, readme: Path.T option}; + dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool, + readme: Path.T option}; fun make_session_info (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents, - doc_prefix1, dump_prefix, remote_path, verbose, readme) = + dump_prefix, remote_path, verbose, readme) = {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents, - doc_prefix1 = doc_prefix1, dump_prefix = dump_prefix, remote_path = remote_path, - verbose = verbose, readme = readme}: session_info; + dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose, + readme = readme}: session_info; (* state *) @@ -290,16 +290,15 @@ val sess_prefix = Path.make path; val html_prefix = Path.append (Path.expand output_path) sess_prefix; - val (doc_prefix1, documents) = - if doc = "" then (NONE, []) + val documents = + if doc = "" then [] else if not (can File.check_dir document_path) then - (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); - (NONE, [])) - else (SOME (Path.append html_prefix document_path, html_prefix), - read_variants doc_variants); + (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); []) + else read_variants doc_variants; val parent_index_path = Path.append Path.parent index_path; - val index_up_lnk = if first_time then + 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 = @@ -309,12 +308,13 @@ val docs = (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ - map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; + map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; val index_text = HTML.begin_index (index_up_lnk, parent_name) (Url.File index_path, session_name) docs (Url.explode "medium.html"); in - session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, - info, doc, doc_graph, documents, doc_prefix1, dump_prefix, remote_path, verbose, readme)); + session_info := + SOME (make_session_info (name, parent_name, session_name, path, html_prefix, + info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme)); browser_info := init_browser_info remote_path path thys; add_html_index (0, index_text) end); @@ -366,8 +366,8 @@ fun finish () = CRITICAL (fn () => - with_session () (fn {name, info, html_prefix, doc_format, doc_graph, - documents, doc_prefix1, dump_prefix, path, verbose, readme, ...} => + with_session () (fn {name, info, html_prefix, doc_format, doc_graph, documents, + dump_prefix, path, verbose, readme, ...} => let val {theories, files, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; @@ -379,7 +379,7 @@ val sorted_graph = sorted_index graph; val opt_graphs = - if doc_graph andalso (is_some doc_prefix1 orelse is_some dump_prefix) then + if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then SOME (isabelle_browser sorted_graph) else NONE; @@ -393,38 +393,43 @@ File.write (Path.append path graph_eps_path) eps)); write_tex_index tex_index path; List.app (finish_tex path) thys); + val _ = + if info then + (Isabelle_System.mkdirs (Path.append html_prefix session_path); + File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer 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 html_prefix); + write_graph sorted_graph (Path.append html_prefix graph_path); + Isabelle_System.isabelle_tool "browser" "-b"; + File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; + List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) + (HTML.applet_pages name (Url.File index_path, name)); + File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; + List.app finish_html thys; + List.app (uncurry File.write) files; + if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") + else ()) + else (); + + val _ = + (case dump_prefix of NONE => () | SOME (cp, path) => + (prepare_sources cp path; + if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") + else ())); + + val doc_paths = + documents |> map (fn (name, tags) => + let + val path = Path.append html_prefix document_path; + val _ = prepare_sources true path; + in isabelle_document true doc_format name tags path html_prefix end); + val _ = + if verbose then + doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n")) + else (); in - if info then - (Isabelle_System.mkdirs (Path.append html_prefix session_path); - File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer 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 html_prefix); - write_graph sorted_graph (Path.append html_prefix graph_path); - Isabelle_System.isabelle_tool "browser" "-b"; - File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; - List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) - (HTML.applet_pages name (Url.File index_path, name)); - File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; - List.app finish_html thys; - List.app (uncurry File.write) files; - if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ()) - else (); - - (case dump_prefix of NONE => () | SOME (cp, path) => - (prepare_sources cp path; - if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ())); - - (case doc_prefix1 of NONE => () | SOME (path, result_path) => - documents |> List.app (fn (name, tags) => - let - val _ = prepare_sources true path; - val doc_path = isabelle_document true doc_format name tags path result_path; - in - if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else () - end)); - browser_info := empty_browser_info; session_info := NONE end));