534 List(HTML.title(title + Isabelle_System.isabelle_heading())), |
534 List(HTML.title(title + Isabelle_System.isabelle_heading())), |
535 context.head(title, List(HTML.par(document_links))) :: |
535 context.head(title, List(HTML.par(document_links))) :: |
536 context.contents("Theories", theories), |
536 context.contents("Theories", theories), |
537 root = Some(context.root_dir)) |
537 root = Some(context.root_dir)) |
538 } |
538 } |
|
539 |
|
540 |
|
541 /* build */ |
|
542 |
|
543 def build( |
|
544 browser_info: Config, |
|
545 store: Sessions.Store, |
|
546 deps: Sessions.Deps, |
|
547 presentation_sessions: List[String], |
|
548 progress: Progress = new Progress, |
|
549 verbose: Boolean = false |
|
550 ): Unit = { |
|
551 val presentation_dir = browser_info.dir(store) |
|
552 progress.echo("Presentation in " + presentation_dir.absolute) |
|
553 update_root(presentation_dir) |
|
554 |
|
555 val chapter_infos = |
|
556 presentation_sessions.map(deps.sessions_structure.apply).groupBy(_.chapter) |
|
557 |
|
558 for ((chapter, infos) <- chapter_infos.iterator) { |
|
559 val entries = infos.map(info => (info.name, info.description)) |
|
560 update_chapter(presentation_dir, chapter, entries) |
|
561 } |
|
562 |
|
563 using(Export.open_database_context(store)) { database_context => |
|
564 val document_info = Document_Info.read(database_context, deps, presentation_sessions) |
|
565 |
|
566 Par_List.map({ (session: String) => |
|
567 progress.expose_interrupt() |
|
568 |
|
569 val build_context = |
|
570 context(deps.sessions_structure, elements1, |
|
571 root_dir = presentation_dir, document_info = document_info) |
|
572 |
|
573 using(database_context.open_session(deps.base_info(session))) { session_context => |
|
574 session_html(build_context, session_context, progress = progress, verbose = verbose) |
|
575 } |
|
576 }, presentation_sessions) |
|
577 } |
|
578 } |
539 } |
579 } |