src/Pure/Tools/build.scala
changeset 73036 b028e8d22d8d
parent 73022 38528017e4c8
child 73055 3e4df2e689ff
equal deleted inserted replaced
73035:03e78b35ebbc 73036:b028e8d22d8d
   513           for ((_, (session_name, _)) <- presentation_chapters) {
   513           for ((_, (session_name, _)) <- presentation_chapters) {
   514             progress.expose_interrupt()
   514             progress.expose_interrupt()
   515             progress.echo("Presenting " + session_name + " ...")
   515             progress.echo("Presenting " + session_name + " ...")
   516             Presentation.session_html(
   516             Presentation.session_html(
   517               resources, session_name, deps, db_context, progress = progress,
   517               resources, session_name, deps, db_context, progress = progress,
   518               verbose = verbose, html_context = html_context, presentation = presentation)
   518               verbose = verbose, html_context = html_context,
       
   519               html_elements = Presentation.html_elements1, presentation = presentation)
   519           })
   520           })
   520 
   521 
   521         val browser_chapters =
   522         val browser_chapters =
   522           presentation_chapters.groupBy(_._1).
   523           presentation_chapters.groupBy(_._1).
   523             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   524             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)