# HG changeset patch
# User wenzelm
# Date 1663870837 -7200
# Node ID 769a7cd5a16ad61020fc7d1b7f7d526948cfff2a
# Parent  005abcb34849fb9779b7a609b8d6b2036b8950e8
clarified signature: re-use store/cache from build results;

diff -r 005abcb34849 -r 769a7cd5a16a src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Sep 22 20:04:57 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Sep 22 20:20:37 2022 +0200
@@ -65,8 +65,6 @@
 
       progress.echo("Running Mirabelle on " + Isabelle_System.identification() + "...")
 
-      val store = Sessions.store(build_options)
-
       def session_setup(session_name: String, session: Session): Unit = {
         session.all_messages +=
           Session.Consumer[Prover.Message]("mirabelle_export") {
@@ -77,7 +75,7 @@
                     progress.echo(
                       "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")")
                   }
-                  val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = store.cache)
+                  val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = build_results0.cache)
                   val lines = Pretty.string_of(yxml).trim()
                   val prefix =
                     Export.explode_name(args.name) match {
diff -r 005abcb34849 -r 769a7cd5a16a src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Thu Sep 22 20:04:57 2022 +0200
+++ b/src/Pure/Admin/build_doc.scala	Thu Sep 22 20:20:37 2022 +0200
@@ -18,8 +18,6 @@
     sequential: Boolean = false,
     docs: List[String] = Nil
   ): Unit = {
-    val store = Sessions.store(options)
-
     val sessions_structure = Sessions.load_structure(options)
     val selected =
       for {
@@ -39,8 +37,9 @@
     }
 
     progress.echo("Build started for sessions " + commas_quote(selection.sessions))
-    Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).ok ||
-      error("Build failed")
+    val build_results =
+      Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs)
+    if (!build_results.ok) error("Build failed")
 
     progress.echo("Build started for documentation " + commas_quote(documents))
     val doc_options = options + "document=pdf"
@@ -54,7 +53,7 @@
             progress.expose_interrupt()
             progress.echo("Documentation " + quote(doc) + " ...")
 
-            using(Export.open_session_context(store, deps.base_info(session))) {
+            using(Export.open_session_context(build_results.store, deps.base_info(session))) {
               session_context =>
                 Document_Build.build_documents(
                   Document_Build.context(session_context),
diff -r 005abcb34849 -r 769a7cd5a16a src/Pure/Thy/document_build.scala
--- 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)
           }
         }
       })
diff -r 005abcb34849 -r 769a7cd5a16a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 20:04:57 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 20:20:37 2022 +0200
@@ -137,9 +137,12 @@
   /** build with results **/
 
   class Results private[Build](
+    val store: Sessions.Store,
     results: Map[String, (Option[Process_Result], Sessions.Info)],
     val presentation_sessions: List[String]
   ) {
+    def cache: Term.Cache = store.cache
+
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def info(name: String): Sessions.Info = results(name)._2
@@ -461,7 +464,7 @@
           if result.ok && browser_info.enabled(result.info)
         } yield name).toList
 
-      new Results(results, presentation_sessions)
+      new Results(store, results, presentation_sessions)
     }
 
     if (export_files) {