src/Pure/Thy/browser_info.scala
changeset 75947 45f08f13354a
parent 75946 82739e4c1e54
child 75949 b09dab301d72
equal deleted inserted replaced
75946:82739e4c1e54 75947:45f08f13354a
   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 }