src/Pure/Tools/build.scala
changeset 73012 238ddf525da4
parent 72993 6ead333e450d
child 73022 38528017e4c8
equal deleted inserted replaced
73011:4519ba8da368 73012:238ddf525da4
   213     /* session selection and dependencies */
   213     /* session selection and dependencies */
   214 
   214 
   215     val full_sessions =
   215     val full_sessions =
   216       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   216       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
   217 
   217 
       
   218     val full_sessions_selection = full_sessions.imports_selection(selection)
       
   219 
   218     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
   220     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
   219     {
   221     {
   220       val digests =
   222       val digests =
   221         full_sessions(session_name).meta_digest ::
   223         full_sessions(session_name).meta_digest ::
   222         deps.sources(session_name) :::
   224         deps.sources(session_name) :::
   275     val queue = Queue(progress, deps.sessions_structure, store)
   277     val queue = Queue(progress, deps.sessions_structure, store)
   276 
   278 
   277     store.prepare_output_dir()
   279     store.prepare_output_dir()
   278 
   280 
   279     if (clean_build) {
   281     if (clean_build) {
   280       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) {
   282       for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
   281         val (relevant, ok) = store.clean_output(name)
   283         val (relevant, ok) = store.clean_output(name)
   282         if (relevant) {
   284         if (relevant) {
   283           if (ok) progress.echo("Cleaned " + name)
   285           if (ok) progress.echo("Cleaned " + name)
   284           else progress.echo(name + " FAILED to clean")
   286           else progress.echo(name + " FAILED to clean")
   285         }
   287         }
   490 
   492 
   491 
   493 
   492     /* PDF/HTML presentation */
   494     /* PDF/HTML presentation */
   493 
   495 
   494     if (!no_build && !progress.stopped && results.ok) {
   496     if (!no_build && !progress.stopped && results.ok) {
       
   497       val selected = full_sessions_selection.toSet
   495       val presentation_chapters =
   498       val presentation_chapters =
   496         (for {
   499         (for {
   497           session_name <- deps.sessions_structure.build_topological_order.iterator
   500           session_name <- deps.sessions_structure.build_topological_order.iterator
   498           info = results.info(session_name)
   501           info = results.info(session_name)
   499           if presentation.enabled(info) && results(session_name).ok }
   502           if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
   500         yield (info.chapter, (session_name, info.description))).toList
   503         yield (info.chapter, (session_name, info.description))).toList
   501 
   504 
   502       if (presentation_chapters.nonEmpty) {
   505       if (presentation_chapters.nonEmpty) {
   503         val presentation_dir = presentation.dir(store)
   506         val presentation_dir = presentation.dir(store)
   504         progress.echo("Presentation in " + presentation_dir.absolute)
   507         progress.echo("Presentation in " + presentation_dir.absolute)