# HG changeset patch # User wenzelm # Date 1605971240 -3600 # Node ID 8ff7a0e394f9677700db29e85574238c898da321 # Parent 573ccec4dbac3194baff1e32e89985fde8535fae clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds); diff -r 573ccec4dbac -r 8ff7a0e394f9 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Sat Nov 21 15:20:12 2020 +0100 +++ b/src/Pure/Thy/presentation.scala Sat Nov 21 16:07:20 2020 +0100 @@ -235,7 +235,7 @@ session: String, deps: Sessions.Deps, store: Sessions.Store, - presentation: Context): Path = + presentation: Context) = { val info = deps.sessions_structure(session) val options = info.options @@ -249,6 +249,13 @@ Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) + val documents = + using(store.open_database(session))(db => + for { + doc <- info.document_variants + (_, pdf) <- Presentation.read_document(db, session, doc.name) + } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc }) + val links = { val deps_link = @@ -262,8 +269,7 @@ else Nil val document_links = - for (doc <- info.documents) - yield HTML.link(doc.path.pdf, HTML.text(doc.name)) + documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name))) Library.separate(HTML.break ::: HTML.nl, (deps_link :: readme_links ::: document_links). @@ -326,8 +332,6 @@ HTML.div("head", List(HTML.chapter(title), HTML.par(links))) :: (if (theories.isEmpty) Nil else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories)))))) - - session_dir } diff -r 573ccec4dbac -r 8ff7a0e394f9 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Nov 21 15:20:12 2020 +0100 +++ b/src/Pure/Tools/build.scala Sat Nov 21 16:07:20 2020 +0100 @@ -154,6 +154,7 @@ class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet + def infos: List[Sessions.Info] = results.values.map(_._2).toList def cancelled(name: String): Boolean = results(name)._1.isEmpty def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 @@ -448,17 +449,19 @@ /* build results */ - val results0 = - if (deps.is_empty) { - progress.echo_warning("Nothing to build") - Map.empty[String, Result] - } - else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } + val results = + { + val results0 = + if (deps.is_empty) { + progress.echo_warning("Nothing to build") + Map.empty[String, Result] + } + else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } - val results = new Results( (for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap) + } if (export_files) { for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) { @@ -485,24 +488,27 @@ } - /* global browser info */ + /* PDF/HTML presentation */ if (!no_build) { + val presentation_dir = presentation.dir(store) + progress.echo("Presentation in " + presentation_dir.absolute + " ...") + + val presentation_chapters = + for { info <- results.infos if results(info.name).ok && presentation.enabled(info) } + yield { + Presentation.session_html(info.name, deps, store, presentation) + (info.chapter, (info.name, info.description)) + } + val browser_chapters = - (for { - (name, result) <- results0.iterator - if result.ok - info = full_sessions(name) - if presentation.enabled(info) - } yield (info.chapter, (name, info.description))).toList.groupBy(_._1). - map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) - - val dir = presentation.dir(store) + presentation_chapters.groupBy(_._1). + map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) - Presentation.update_chapter_index(dir, chapter, entries) + Presentation.update_chapter_index(presentation_dir, chapter, entries) - if (browser_chapters.nonEmpty) Presentation.make_global_index(dir) + if (browser_chapters.nonEmpty) Presentation.make_global_index(presentation_dir) } results diff -r 573ccec4dbac -r 8ff7a0e394f9 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sat Nov 21 15:20:12 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Sat Nov 21 16:07:20 2020 +0100 @@ -217,33 +217,23 @@ val document_errors = try { - if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) { + if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { + val document_progress = + new Progress { + override def echo(msg: String): Unit = + document_output.synchronized { document_output += msg } + override def echo_document(msg: String): Unit = + progress.echo_document(msg) + } val documents = - if (info.documents.isEmpty) Nil - else { - val document_progress = - new Progress { - override def echo(msg: String): Unit = - document_output.synchronized { document_output += msg } - override def echo_document(msg: String): Unit = - progress.echo_document(msg) - } - val documents = - Presentation.build_documents(session_name, deps, store, verbose = verbose, - verbose_latex = true, progress = document_progress) - using(store.open_database(session_name, output = true))(db => - for ((doc, pdf) <- documents) { - db.transaction { - Presentation.write_document(db, session_name, doc, pdf) - } - }) - documents - } - if (presentation.enabled(info)) { - val dir = Presentation.session_html(session_name, deps, store, presentation) - for ((doc, pdf) <- documents) Bytes.write(dir + doc.path.pdf, pdf) - if (verbose) progress.echo("Browser info at " + dir.absolute) - } + Presentation.build_documents(session_name, deps, store, verbose = verbose, + verbose_latex = true, progress = document_progress) + using(store.open_database(session_name, output = true))(db => + for ((doc, pdf) <- documents) { + db.transaction { + Presentation.write_document(db, session_name, doc, pdf) + } + }) } Nil }