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