src/Pure/Tools/build.scala
changeset 72992 bcba32fd89de
parent 72962 af2d0e07493b
child 72993 6ead333e450d
equal deleted inserted replaced
72991:d0a0b74f0ad7 72992:bcba32fd89de
   508         using(store.open_database_context())(db_context =>
   508         using(store.open_database_context())(db_context =>
   509           for ((_, (session_name, _)) <- presentation_chapters) {
   509           for ((_, (session_name, _)) <- presentation_chapters) {
   510             progress.expose_interrupt()
   510             progress.expose_interrupt()
   511             progress.echo("Presenting " + session_name + " ...")
   511             progress.echo("Presenting " + session_name + " ...")
   512             Presentation.session_html(
   512             Presentation.session_html(
   513               resources, session_name, deps, db_context, html_context, presentation)
   513               resources, session_name, deps, db_context, progress, html_context, presentation)
   514           })
   514           })
   515 
   515 
   516         val browser_chapters =
   516         val browser_chapters =
   517           presentation_chapters.groupBy(_._1).
   517           presentation_chapters.groupBy(_._1).
   518             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   518             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)