499 val presentation_dir = presentation.dir(store) |
499 val presentation_dir = presentation.dir(store) |
500 progress.echo("Presentation in " + presentation_dir.absolute) |
500 progress.echo("Presentation in " + presentation_dir.absolute) |
501 |
501 |
502 val resources = Resources.empty |
502 val resources = Resources.empty |
503 val html_context = Presentation.html_context() |
503 val html_context = Presentation.html_context() |
504 val theory_cache = Presentation.Theory_Cache() |
|
505 |
504 |
506 using(store.open_database_context())(db_context => |
505 using(store.open_database_context())(db_context => |
507 for ((_, (session_name, _)) <- presentation_chapters) { |
506 for ((_, (session_name, _)) <- presentation_chapters) { |
508 progress.expose_interrupt() |
507 progress.expose_interrupt() |
509 progress.echo("Presenting " + session_name + " ...") |
508 progress.echo("Presenting " + session_name + " ...") |
510 Presentation.session_html( |
509 Presentation.session_html( |
511 resources, session_name, deps, db_context, progress = progress, |
510 resources, session_name, deps, db_context, progress = progress, |
512 verbose = verbose, html_context = html_context, |
511 verbose = verbose, html_context = html_context, |
513 elements = Presentation.elements1, presentation = presentation, |
512 elements = Presentation.elements1, presentation = presentation) |
514 theory_cache = theory_cache) |
|
515 }) |
513 }) |
516 |
514 |
517 val browser_chapters = |
515 val browser_chapters = |
518 presentation_chapters.groupBy(_._1). |
516 presentation_chapters.groupBy(_._1). |
519 map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) |
517 map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) |