src/Pure/Thy/browser_info.scala
changeset 75947 45f08f13354a
parent 75946 82739e4c1e54
child 75949 b09dab301d72
--- 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)
+    }
+  }
 }