" "

\n" txt ^ - end_document; - end; diff -r 65554bac121b -r 830222403681 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Thy/html.scala Mon Nov 16 22:23:04 2020 +0100 @@ -155,6 +155,7 @@ def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) val no_text: XML.Tree = XML.Text("") val break: XML.Body = List(XML.elem("br")) + val nl: XML.Body = List(XML.Text("\n")) class Operator(val name: String) { @@ -197,9 +198,11 @@ def description(items: List[(XML.Body, XML.Body)]): XML.Elem = descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) })) - def link(href: String, body: XML.Body = Nil): XML.Elem = + def link(href: String, body: XML.Body): XML.Elem = XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) + def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body) + def image(src: String, alt: String = ""): XML.Elem = XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) diff -r 65554bac121b -r 830222403681 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Thy/present.ML Mon Nov 16 22:23:04 2020 +0100 @@ -1,168 +1,75 @@ (* Title: Pure/Thy/present.ML - Author: Markus Wenzel and Stefan Berghofer, TU Muenchen + Author: Makarius -Theory presentation: HTML and PDF-LaTeX documents. +Theory presentation: HTML and LaTeX documents. *) signature PRESENT = sig - val init: bool -> Path.T -> string list -> string * string -> bool -> unit - val finish: unit -> unit - val begin_theory: int -> HTML.text -> theory -> theory + val document_html_name: theory -> Path.binding + val document_tex_name: theory -> Path.binding + val html_name: theory -> Path.T + val export_html: theory -> Command_Span.span list -> unit end; structure Present: PRESENT = struct - -(** paths **) - -val html_ext = Path.ext "html"; -val html_path = html_ext o Path.basic; -val index_path = Path.basic "index.html"; -val readme_html_path = Path.basic "README.html"; -val session_graph_path = Path.basic "session_graph.pdf"; -val document_path = Path.ext "pdf" o Path.basic; - -fun show_path path = Path.implode (Path.expand (File.full_path Path.current path)); - +(** artefact names **) - -(** global browser info state **) - -(* type browser_info *) - -type browser_info = - {html_theories: string Symtab.table, - html_index: (int * string) list}; - -fun make_browser_info (html_theories, html_index) : browser_info = - {html_theories = html_theories, html_index = html_index}; - -val empty_browser_info = make_browser_info (Symtab.empty, []); +fun document_name ext thy = + Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext); -fun map_browser_info f {html_theories, html_index} = - make_browser_info (f (html_theories, html_index)); - - -(* state *) - -val browser_info = Synchronized.var "browser_info" empty_browser_info; -fun change_browser_info f = Synchronized.change browser_info (map_browser_info f); - -fun update_html name html = change_browser_info (apfst (Symtab.update (name, html))); - -fun add_html_index txt = change_browser_info (apsnd (cons txt)); +val document_html_name = document_name "html"; +val document_tex_name = document_name "tex"; - - -(** global session state **) - -(* session_info *) - -type session_info = - {name: string, chapter: string, info_path: Path.T, info: bool, - verbose: bool, readme: Path.T option}; - -fun make_session_info (name, chapter, info_path, info, verbose, readme) = - {name = name, chapter = chapter, info_path = info_path, info = info, - verbose = verbose, readme = readme}: session_info; +fun html_name thy = Path.basic (Context.theory_name thy ^ ".html"); -(* state *) - -val session_info = Unsynchronized.ref (NONE: session_info option); - -fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); - -val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name; - -fun is_session_theory thy = - (case ! session_info of - NONE => false - | SOME {name, ...} => name = theory_qualifier thy); - - -(** document preparation **) - -(* init session *) - -fun init info info_path documents (chapter, name) verbose = - let - val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; - val symbols = Resources.html_symbols (); - val docs = - (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ - map (fn name => (Url.File (document_path name), name)) documents; - in - session_info := SOME (make_session_info (name, chapter, info_path, info, verbose, readme)); - Synchronized.change browser_info (K empty_browser_info); - add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) - end; - +(* theory as HTML *) -(* finish session -- output all generated text *) - -fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index)); -fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; - -fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} => - let - val {html_theories, html_index} = Synchronized.value browser_info; - - val session_prefix = info_path + Path.basic chapter + Path.basic name; - - fun finish_html (a, html) = File.write (session_prefix + html_path a) html; +local - val _ = - if info then - (Isabelle_System.make_directory session_prefix; - File.write_buffer (session_prefix + index_path) - (index_buffer html_index |> Buffer.add HTML.end_document); - (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix); - Symtab.fold (K o finish_html) html_theories (); - if verbose - then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") - else ()) - else (); - in - Synchronized.change browser_info (K empty_browser_info); - session_info := NONE - end); - - -(* theory elements *) - -fun theory_link (curr_chapter, curr_session) thy = +fun get_session_chapter thy = let val session = Resources.theory_qualifier (Context.theory_long_name thy); val chapter = Resources.session_chapter session; - val link = html_path (Context.theory_name thy); + in (session, chapter) end; + +fun theory_link thy thy' = + let + val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy'); + val link = html_name thy'; in - if curr_session = session then SOME link - else if curr_chapter = chapter then - SOME (Path.parent + Path.basic session + link) + if session = session' then SOME link + else if chapter = chapter' then SOME (Path.parent + Path.basic session + link) else if chapter = Context.PureN then NONE else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) end; -fun begin_theory update_time html thy = - with_session_info thy (fn {name = session_name, chapter, ...} => - let - val name = Context.theory_name thy; +fun theory_document symbols A Bs body = + HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^ + HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "
\n" ^ + HTML.keyword symbols "imports" ^ " " ^ + space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^ + "
\n\n

" ::
+  body @ ["

\n", HTML.end_document]; + +in - val parent_specs = - Theory.parents_of thy |> map (fn parent => - (Option.map Url.File (theory_link (chapter, session_name) parent), - (Context.theory_name parent))); +fun export_html thy spans = + let + val name = Context.theory_name thy; + val parents = + Theory.parents_of thy |> map (fn thy' => + (Option.map Url.File (theory_link thy thy'), Context.theory_name thy')); - val symbols = Resources.html_symbols (); - val _ = update_html name (HTML.theory symbols name parent_specs html); - - val _ = - if is_session_theory thy then - add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)) - else (); - in thy end); + val symbols = Resources.html_symbols (); + val keywords = Thy_Header.get_keywords thy; + val body = map (HTML.present_span symbols keywords) spans; + val html = XML.blob (theory_document symbols name parents body); + in Export.export thy (document_html_name thy) html end end; + +end; diff -r 65554bac121b -r 830222403681 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Thy/present.scala Mon Nov 16 22:23:04 2020 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/Thy/present.scala Author: Makarius -Theory presentation: HTML. +Theory presentation: HTML and LaTeX documents. */ package isabelle @@ -74,27 +74,72 @@ } - /* finish session */ + /* present session */ + + val session_graph_path = Path.explode("session_graph.pdf") + val readme_path = Path.basic("README.html") + + def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html" + def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name) + + def theory_link(name: Document.Node.Name): XML.Tree = + HTML.link(html_name(name), HTML.text(name.theory_base_name)) - def finish( - browser_info: Path, - graph_pdf: Bytes, - info: Sessions.Info, - name: String) + def session_html(session: String, deps: Sessions.Deps, store: Sessions.Store): Path = { - val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) - val session_fonts = session_prefix + Path.explode("fonts") + val info = deps.sessions_structure(session) + val options = info.options + val base = deps(session) + + val session_dir = store.browser_info + info.chapter_session + val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts")) + for (entry <- Isabelle_Fonts.fonts(hidden = true)) + File.copy(entry.path, session_fonts) + + Bytes.write(session_dir + session_graph_path, + graphview.Graph_File.make_pdf(options, base.session_graph_display)) + + val links = + { + val deps_link = + HTML.link(session_graph_path, HTML.text("theory dependencies")) - if (info.options.bool("browser_info")) { - Isabelle_System.make_directory(session_fonts) + val readme_links = + if ((info.dir + readme_path).is_file) { + File.copy(info.dir + readme_path, session_dir + readme_path) + List(HTML.link(readme_path, HTML.text("README"))) + } + else Nil - Bytes.write(session_prefix + session_graph_path, graph_pdf) + val document_links = + for ((name, _) <- info.documents) + yield HTML.link(Path.basic(name).pdf, HTML.text(name)) + + Library.separate(HTML.break ::: HTML.nl, + (deps_link :: readme_links ::: document_links). + map(link => HTML.text("View ") ::: List(link))).flatten + } - HTML.write_isabelle_css(session_prefix) + val theories = + using(store.open_database(session))(db => + for { + name <- base.session_theories + entry <- Export.read_entry(db, session, name.theory, document_html_name(name)) + } yield name -> entry.uncompressed(cache = store.xz_cache)) + + val theories_body = + HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name))) - for (entry <- Isabelle_Fonts.fonts(hidden = true)) - File.copy(entry.path, session_fonts) - } + val title = "Session " + session + HTML.write_document(session_dir, "index.html", + List(HTML.title(title + " (" + Distribution.version + ")")), + HTML.div("head", List(HTML.chapter(title), HTML.par(links))) :: + (if (theories.isEmpty) Nil + else List(HTML.div("theories", List(HTML.section("Theories"), theories_body))))) + + for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html) + + session_dir } @@ -193,7 +238,6 @@ /** build documents **/ val session_tex_path = Path.explode("session.tex") - val session_graph_path = Path.explode("session_graph.pdf") def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name) @@ -331,7 +375,7 @@ } if (info.options.bool("browser_info") || doc_output.isEmpty) { - output(store.browser_info + Path.basic(info.chapter) + Path.basic(session)) + output(store.browser_info + info.chapter_session) } doc_output.foreach(output) diff -r 65554bac121b -r 830222403681 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Nov 16 22:23:04 2020 +0100 @@ -459,6 +459,8 @@ export_files: List[(Path, Int, List[String])], meta_digest: SHA1.Digest) { + def chapter_session: Path = Path.basic(chapter) + Path.basic(name) + def deps: List[String] = parent.toList ::: imports def deps_base(session_bases: String => Base): Base = diff -r 65554bac121b -r 830222403681 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Thy/thy_info.ML Mon Nov 16 22:23:04 2020 +0100 @@ -53,6 +53,7 @@ val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => + (Present.export_html thy (map #span segments); if exists (Toplevel.is_skipped_proof o #state) segments then () else let @@ -62,12 +63,12 @@ else let val thy_name = Context.theory_name thy; - val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex"); + val document_tex_name = Present.document_tex_name thy; val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; in Export.export thy document_tex_name (XML.blob output) end - end)); + end))); @@ -302,13 +303,7 @@ val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; - val symbols = Resources.html_symbols (); - val html = implode (map (HTML.present_span symbols keywords) spans); - - fun init () = - Resources.begin_theory master_dir header parents - |> Present.begin_theory update_time html; - + fun init () = Resources.begin_theory master_dir header parents; val (results, thy) = cond_timeit true ("theory " ^ quote name) (fn () => excursion keywords master_dir last_timing init elements); diff -r 65554bac121b -r 830222403681 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Tools/build.ML Mon Nov 16 22:23:04 2020 +0100 @@ -86,25 +86,23 @@ Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let - val (html_symbols, (command_timings, (verbose, (browser_info, - (documents, (parent_name, (chapter, (session_name, (master_dir, - (theories, (session_positions, (session_directories, (session_chapters, - (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = + val (html_symbols, (command_timings, (parent_name, (chapter, + (session_name, (master_dir, (theories, (session_positions, (session_directories, + (session_chapters, (doc_names, + (global_theories, (loaded_theories, bibtex_entries))))))))))))) = YXML.parse_body args_yxml |> let open XML.Decode; val position = Position.of_properties o properties; val path = Path.explode o string; in - pair (list (pair string int)) (pair (list properties) (pair bool (pair path - (pair (list string) (pair string (pair string (pair string - (pair path - (pair (((list (pair Options.decode (list (pair string position)))))) - (pair (list (pair string properties)) - (pair (list (pair string string)) - (pair (list (pair string string)) (pair (list string) - (pair (list (pair string string)) (pair (list string) - (list (pair string (list string)))))))))))))))))) + pair (list (pair string int)) (pair (list properties) (pair string (pair string + (pair string (pair path + (pair (((list (pair Options.decode (list (pair string position)))))) + (pair (list (pair string properties)) (pair (list (pair string string)) + (pair (list (pair string string)) (pair (list string) + (pair (list (pair string string)) (pair (list string) + (list (pair string (list string))))))))))))))) end; fun build () = @@ -120,14 +118,7 @@ global_theories = global_theories, loaded_theories = loaded_theories}; - val _ = - Session.init - (Options.default_bool "browser_info") - browser_info - documents - parent_name - (chapter, session_name) - verbose; + val _ = Session.init parent_name (chapter, session_name); val last_timing = get_timings (fold update_timings command_timings empty_timings); diff -r 65554bac121b -r 830222403681 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Tools/build.scala Mon Nov 16 22:23:04 2020 +0100 @@ -165,7 +165,6 @@ val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure - private val documents = info.documents.map(_._1) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { @@ -175,23 +174,22 @@ YXML.string_of_body( { import XML.Encode._ - pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, - pair(list(string), pair(string, pair(string, pair(string, pair(Path.encode, + pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string, + pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), - pair(list(string), list(pair(string, list(string)))))))))))))))))))( - (Symbol.codes, (command_timings0, (verbose, (store.browser_info, - (documents, (parent, (info.chapter, (session_name, (Path.current, - (info.theories, + pair(list(string), list(pair(string, list(string))))))))))))))))( + (Symbol.codes, (command_timings0, (parent, (info.chapter, + (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, (base.doc_names, (base.global_theories.toList, - (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))))) + (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))) }) val env = @@ -373,20 +371,23 @@ val document_errors = try { - if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && documents.nonEmpty) { - val document_progress = - new Progress { - override def echo(msg: String): Unit = - document_output.synchronized { document_output += msg } - override def echo_document(path: Path): Unit = - progress.echo_document(path) - } - Present.build_documents(session_name, deps, store, verbose = verbose, - verbose_latex = true, progress = document_progress) + if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) { + if (info.documents.nonEmpty) { + val document_progress = + new Progress { + override def echo(msg: String): Unit = + document_output.synchronized { document_output += msg } + override def echo_document(path: Path): Unit = + progress.echo_document(path) + } + Present.build_documents(session_name, deps, store, verbose = verbose, + verbose_latex = true, progress = document_progress) + } + if (info.options.bool("browser_info")) { + val dir = Present.session_html(session_name, deps, store) + if (verbose) progress.echo("Browser info at " + dir.absolute) + } } - val graph_pdf = - graphview.Graph_File.make_pdf(options, deps(session_name).session_graph_display) - Present.finish(store.browser_info, graph_pdf, info, session_name) Nil } catch { case Exn.Interrupt.ERROR(msg) => List(msg) }