diff -r f49c4f160b84 -r 0e5339342998 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Aug 06 17:16:19 2022 +0200 +++ b/src/Pure/Tools/build.scala Sat Aug 06 17:28:59 2022 +0200 @@ -495,10 +495,8 @@ } using(Export.open_context(store)) { export_context => - val db_context = export_context.db_context - val presentation_nodes = - Presentation.Nodes.read(presentation_sessions.map(_.name), deps, db_context) + Presentation.Nodes.read(export_context, deps, presentation_sessions.map(_.name)) Par_List.map({ (session: String) => progress.expose_interrupt() @@ -512,8 +510,7 @@ deps.sessions_structure(deps(session).theory_qualifier(name)) } - val session_base_info = deps.base_info(session) - using(export_context.open_session(session_base_info)) { session_context => + using(export_context.open_session(deps.base_info(session))) { session_context => Presentation.session_html(session_context, deps, progress = progress, verbose = verbose,