clarified modules and options (from store);

--- a/src/Pure/Build/build_job.scala	Tue Apr 16 16:27:40 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Apr 16 16:53:10 2024 +0200
@@ -23,20 +23,6 @@
 
   /* build session */
 
-  def store_heaps(
-    store: Store,
-    options: Options,
-    session: Store.Session,
-    database_server: Option[SQL.Database] = None,
-    server: SSH.Server = SSH.no_server,
-    progress: Progress = new Progress
-  ): Unit = {
-    store.maybe_using_heaps_database(database_server, server = server) { db =>
-      val slice = Space.MiB(options.real("build_database_slice"))
-      ML_Heap.store(db, session, slice, cache = store.cache.compress, progress = progress)
-    }
-  }
-
   def start_session(
     build_context: Build.Context,
     session_context: Session_Context,
@@ -528,8 +514,8 @@
             case None => using(store.open_database(session_name, output = true))(write_info)
           }
 
-          store_heaps(store, options, store_session,
-            database_server = database_server, server = server, progress = progress)
+          store.in_heaps_database(
+            List(store_session), database_server, server = server, progress = progress)
 
           // messages
           process_result.err_lines.foreach(progress.echo(_))

--- a/src/Pure/Build/store.scala	Tue Apr 16 16:27:40 2024 +0200
+++ b/src/Pure/Build/store.scala	Tue Apr 16 16:53:10 2024 +0200
@@ -395,6 +395,18 @@
     }
   }
 
+  def in_heaps_database(
+    sessions: List[Store.Session],
+    database_server: Option[SQL.Database],
+    server: SSH.Server = SSH.no_server,
+    progress: Progress = new Progress
+  ): Unit = {
+    maybe_using_heaps_database(database_server, server = server) { db =>
+      val slice = Space.MiB(options.real("build_database_slice"))
+      sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress))
+    }
+  }
+
   def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database =
     if (build_database_server || build_cluster) open_database_server(server = server)
     else SQLite.open_database(path, restrict = true)