# HG changeset patch
# User wenzelm
# Date 1636113349 -3600
# Node ID 2bc24136bdeb0788726fa2900cfe994146bf5338
# Parent  decf8b66e2fbd5ca38df2ce3612a3fd599d2d4f7
clarified order: prefer bottom-up construction of partial content;

diff -r decf8b66e2fb -r 2bc24136bdeb src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Nov 05 12:36:00 2021 +0100
+++ b/src/Pure/Tools/build.scala	Fri Nov 05 12:55:49 2021 +0100
@@ -144,7 +144,8 @@
     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
+    def get_info(name: String): Option[Sessions.Info] = results.get(name).map(_._2)
+    def info(name: String): Sessions.Info = get_info(name).get
     val rc: Int =
       results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
         foldLeft(Process_Result.RC.ok)(_ max _)
@@ -490,14 +491,20 @@
       val selected = full_sessions_selection.toSet
       val presentation_sessions =
         (for {
-          session_name <- deps.sessions_structure.build_topological_order.iterator
-          info = results.info(session_name)
+          session_name <- deps.sessions_structure.imports_topological_order.iterator
+          info <- results.get_info(session_name)
           if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
         yield info).toList
 
       if (presentation_sessions.nonEmpty) {
         val presentation_dir = presentation.dir(store)
         progress.echo("Presentation in " + presentation_dir.absolute)
+        Presentation.update_global_index(presentation_dir)
+
+        for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) {
+          val entries = infos.map(info => (info.name, info.description))
+          Presentation.update_chapter_index(presentation_dir, chapter, entries)
+        }
 
         val resources = Resources.empty
         val html_context = Presentation.html_context()
@@ -511,17 +518,6 @@
               verbose = verbose, html_context = html_context,
               elements = Presentation.elements1, presentation = presentation)
           })
-
-        val browser_chapters =
-          (for {
-            (chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator
-            if infos.nonEmpty
-          } yield (chapter, infos.map(info => (info.name, info.description)))).toList
-
-        for ((chapter, entries) <- browser_chapters)
-          Presentation.update_chapter_index(presentation_dir, chapter, entries)
-
-        if (browser_chapters.nonEmpty) Presentation.update_global_index(presentation_dir)
       }
     }