# HG changeset patch
# User wenzelm
# Date 1672671736 -3600
# Node ID a17f9ff37558c0084121bfa86f349e06dfa0059e
# Parent  c6cdf2a641f4b51d196918b5e985975269a2c0f4
clarified session_sources (again, see also 9d0e6ea7aa68);

diff -r c6cdf2a641f4 -r a17f9ff37558 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jan 02 15:41:50 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Jan 02 16:02:16 2023 +0100
@@ -1578,10 +1578,12 @@
     def write_session_info(
       db: SQL.Database,
       session_name: String,
+      sources: Sources.T,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info
     ): Unit = {
       db.transaction {
+        write_sources(db, session_name, sources)
         db.using_statement(Session_Info.table.insert()) { stmt =>
           stmt.string(1) = session_name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
@@ -1647,18 +1649,15 @@
 
     /* session sources */
 
-    def write_sources(db: SQL.Database, session_base: Base): Unit = {
-      val files = Sources.read_files(session_base, cache = cache.compress)
-      db.transaction {
-        for ((name, file) <- files) {
-          db.using_statement(Sources.table.insert()) { stmt =>
-            stmt.string(1) = session_base.session_name
-            stmt.string(2) = name
-            stmt.string(3) = file.digest.toString
-            stmt.bool(4) = file.compressed
-            stmt.bytes(5) = file.body
-            stmt.execute()
-          }
+    def write_sources(db: SQL.Database, session_name: String, files: Sources.T): Unit = {
+      for ((name, file) <- files) {
+        db.using_statement(Sources.table.insert()) { stmt =>
+          stmt.string(1) = session_name
+          stmt.string(2) = name
+          stmt.string(3) = file.digest.toString
+          stmt.bool(4) = file.compressed
+          stmt.bytes(5) = file.body
+          stmt.execute()
         }
       }
     }
diff -r c6cdf2a641f4 -r a17f9ff37558 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jan 02 15:41:50 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 02 16:02:16 2023 +0100
@@ -348,7 +348,7 @@
 
             // write database
             using(store.open_database(session_name, output = true))(db =>
-              store.write_session_info(db, session_name,
+              store.write_session_info(db, session_name, job.session_sources,
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
@@ -418,17 +418,13 @@
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
-                  val session_background = build_deps.background(session_name)
-
                   store.clean_output(session_name)
-                  using(store.open_database(session_name, output = true)) { db =>
-                    store.init_session_info(db, session_name)
-                    store.write_sources(db, session_background.base)
-                  }
+                  using(store.open_database(session_name, output = true))(
+                    store.init_session_info(_, session_name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
-                    new Build_Job(progress, session_background, store, do_store,
+                    new Build_Job(progress, build_deps.background(session_name), store, do_store,
                       log, session_setup, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
diff -r c6cdf2a641f4 -r a17f9ff37558 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Jan 02 15:41:50 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Jan 02 16:02:16 2023 +0100
@@ -246,6 +246,9 @@
   val info: Sessions.Info = session_background.sessions_structure(session_name)
   val options: Options = NUMA.policy_options(info.options, numa_node)
 
+  val session_sources: Sessions.Sources.T =
+    Sessions.Sources.read_files(session_background.base, cache = store.cache.compress)
+
   private val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")