# HG changeset patch
# User wenzelm
# Date 1663839930 -7200
# Node ID fb4215da4919becf5eb8c79f0e3ce543ae752954
# Parent  544e81a2c9fc5125720828779a06783c8ccd3674
clarified presentation_sessions: work with partial results;

diff -r 544e81a2c9fc -r fb4215da4919 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 11:30:12 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 11:45:30 2022 +0200
@@ -136,7 +136,10 @@
 
   /** build with results **/
 
-  class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) {
+  class Results private[Build](
+    results: Map[String, (Option[Process_Result], Sessions.Info)],
+    val presentation_sessions: List[String]
+  ) {
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def info(name: String): Sessions.Info = results(name)._2
@@ -235,13 +238,6 @@
 
     val build_sessions = build_deps.sessions_structure
 
-    val presentation_sessions =
-      (for {
-        session_name <- build_sessions.build_topological_order.iterator
-        info <- build_sessions.get(session_name)
-        if full_sessions_selected(session_name) && browser_info.enabled(info) }
-      yield session_name).toList
-
 
     /* check unknown files */
 
@@ -457,7 +453,14 @@
         (for ((name, result) <- results0.iterator)
           yield (name, (result.process, result.info))).toMap
 
-      new Results(results1)
+      val presentation_sessions =
+        (for {
+          name <- build_sessions.build_topological_order.iterator
+          result <- results0.get(name)
+          if result.ok && browser_info.enabled(result.info)
+        } yield name).toList
+
+      new Results(results1, presentation_sessions)
     }
 
     if (export_files) {
@@ -475,6 +478,11 @@
       }
     }
 
+    if (!no_build && !progress.stopped && results.presentation_sessions.nonEmpty) {
+      Browser_Info.build(browser_info, store, build_deps, results.presentation_sessions,
+        progress = progress, verbose = verbose)
+    }
+
     if (!results.ok && (verbose || !no_build)) {
       val unfinished =
         (for {
@@ -484,11 +492,6 @@
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
-    if (!no_build && !progress.stopped && results.ok && presentation_sessions.nonEmpty) {
-      Browser_Info.build(browser_info, store, build_deps, presentation_sessions,
-        progress = progress, verbose = verbose)
-    }
-
     results
   }