src/Pure/Thy/document_build.scala
changeset 76206 769a7cd5a16a
parent 75941 4bbbbaa656f1
child 76370 9bd948666e8a
--- a/src/Pure/Thy/document_build.scala	Thu Sep 22 20:04:57 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Thu Sep 22 20:20:37 2022 +0200
@@ -480,13 +480,12 @@
           }
 
         val progress = new Console_Progress(verbose = verbose_build)
-        val store = Sessions.store(options)
 
         progress.interrupt_handler {
-          val res =
+          val build_results =
             Build.build(options, selection = Sessions.Selection.session(session),
               dirs = dirs, progress = progress, verbose = verbose_build)
-          if (!res.ok) error("Failed to build session " + quote(session))
+          if (!build_results.ok) error("Failed to build session " + quote(session))
 
           val deps =
             Sessions.load_structure(options + "document=pdf", dirs = dirs).
@@ -498,11 +497,12 @@
             progress.echo_warning("No output directory")
           }
 
-          using(Export.open_session_context(store, session_base_info)) { session_context =>
-            build_documents(
-              context(session_context, progress = progress),
-              output_sources = output_sources, output_pdf = output_pdf,
-              verbose = verbose_latex)
+          using(Export.open_session_context(build_results.store, session_base_info)) {
+            session_context =>
+              build_documents(
+                context(session_context, progress = progress),
+                output_sources = output_sources, output_pdf = output_pdf,
+                verbose = verbose_latex)
           }
         }
       })