diff -r 7c3d50ffaece -r 93ccf8b7a660 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Jan 04 13:21:45 2023 +0100 +++ b/src/Pure/Tools/build.scala Wed Jan 04 13:39:40 2023 +0100 @@ -139,8 +139,8 @@ class Results private[Build]( val store: Sessions.Store, val deps: Sessions.Deps, - results: Map[String, (Option[Process_Result], Sessions.Info)], - val presentation_sessions: Browser_Info.Config => List[String] + val sessions_ok: List[String], + results: Map[String, (Option[Process_Result], Sessions.Info)] ) { def cache: Term.Cache = store.cache @@ -452,18 +452,18 @@ } else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } + val sessions_ok: List[String] = + (for { + name <- build_deps.sessions_structure.build_topological_order.iterator + result <- build_results.get(name) + if result.ok + } yield name).toList + val results = (for ((name, result) <- build_results.iterator) yield (name, (result.process, result.info))).toMap - def presentation_sessions(config: Browser_Info.Config): List[String] = - (for { - name <- build_deps.sessions_structure.build_topological_order.iterator - result <- build_results.get(name) - if result.ok && config.enabled(result.info) - } yield name).toList - - new Results(store, build_deps, results, presentation_sessions) + new Results(store, build_deps, sessions_ok, results) } if (export_files) { @@ -481,7 +481,8 @@ } } - val presentation_sessions = results.presentation_sessions(browser_info) + val presentation_sessions = + results.sessions_ok.filter(name => browser_info.enabled(results.info(name))) if (presentation_sessions.nonEmpty && !progress.stopped) { Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions, progress = progress, verbose = verbose)