# HG changeset patch
# User wenzelm
# Date 1661080345 -7200
# Node ID 45f08f13354a16ff7c4215ca0415f96cebdf1cad
# Parent  82739e4c1e5472dcd843d6efeed4fe34855de1f9
clarified modules;

diff -r 82739e4c1e54 -r 45f08f13354a src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:53:46 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 21 13:12:25 2022 +0200
@@ -536,4 +536,44 @@
           context.contents("Theories", theories),
         root = Some(context.root_dir))
   }
+
+
+  /* build */
+
+  def build(
+    browser_info: Config,
+    store: Sessions.Store,
+    deps: Sessions.Deps,
+    presentation_sessions: List[String],
+    progress: Progress = new Progress,
+    verbose: Boolean = false
+  ): Unit = {
+    val presentation_dir = browser_info.dir(store)
+    progress.echo("Presentation in " + presentation_dir.absolute)
+    update_root(presentation_dir)
+
+    val chapter_infos =
+      presentation_sessions.map(deps.sessions_structure.apply).groupBy(_.chapter)
+
+    for ((chapter, infos) <- chapter_infos.iterator) {
+      val entries = infos.map(info => (info.name, info.description))
+      update_chapter(presentation_dir, chapter, entries)
+    }
+
+    using(Export.open_database_context(store)) { database_context =>
+      val document_info = Document_Info.read(database_context, deps, presentation_sessions)
+
+      Par_List.map({ (session: String) =>
+        progress.expose_interrupt()
+
+        val build_context =
+          context(deps.sessions_structure, elements1,
+            root_dir = presentation_dir, document_info = document_info)
+
+        using(database_context.open_session(deps.base_info(session))) { session_context =>
+          session_html(build_context, session_context, progress = progress, verbose = verbose)
+        }
+      }, presentation_sessions)
+    }
+  }
 }
diff -r 82739e4c1e54 -r 45f08f13354a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Aug 21 12:53:46 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sun Aug 21 13:12:25 2022 +0200
@@ -239,7 +239,7 @@
         session_name <- deps.sessions_structure.build_topological_order.iterator
         info <- deps.sessions_structure.get(session_name)
         if full_sessions_selected(session_name) && browser_info.enabled(info) }
-      yield info).toList
+      yield session_name).toList
 
 
     /* check unknown files */
@@ -481,38 +481,9 @@
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
-
-    /* PDF/HTML presentation */
-
-    if (!no_build && !progress.stopped && results.ok) {
-      if (presentation_sessions.nonEmpty) {
-        val presentation_dir = browser_info.dir(store)
-        progress.echo("Presentation in " + presentation_dir.absolute)
-        Browser_Info.update_root(presentation_dir)
-
-        for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) {
-          val entries = infos.map(info => (info.name, info.description))
-          Browser_Info.update_chapter(presentation_dir, chapter, entries)
-        }
-
-        using(Export.open_database_context(store)) { database_context =>
-          val document_info =
-            Document_Info.read(database_context, deps, presentation_sessions.map(_.name))
-
-          Par_List.map({ (session: String) =>
-            progress.expose_interrupt()
-
-            val context =
-              Browser_Info.context(deps.sessions_structure, Browser_Info.elements1,
-                root_dir = presentation_dir, document_info = document_info)
-
-            using(database_context.open_session(deps.base_info(session))) { session_context =>
-              Browser_Info.session_html(context, session_context,
-                progress = progress, verbose = verbose)
-            }
-          }, presentation_sessions.map(_.name))
-        }
-      }
+    if (!no_build && !progress.stopped && results.ok && presentation_sessions.nonEmpty) {
+      Browser_Info.build(browser_info, store, deps, presentation_sessions,
+        progress = progress, verbose = verbose)
     }
 
     results