clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);

--- 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
   }
 
 

--- 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

--- 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
         }