src/Pure/Tools/build_job.scala

 
   def start_session(
     build_context: Build_Process.Context,
     progress: Progress,
     log: Logger,
+    database_server: Option[SQL.Database],
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
     node_info: Host.Node_Info
   ): Session_Job = {
-    new Session_Job(build_context, progress, log, session_background, input_shasum, node_info)
+    new Session_Job(build_context, progress, log, database_server,
+      session_background, input_shasum, node_info)
   }
 
   object Session_Context {
     def load(
       build_uuid: String,

 
   class Session_Job private[Build_Job](
     build_context: Build_Process.Context,
     progress: Progress,
     log: Logger,
+    database_server: Option[SQL.Database],
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
     node_info: Host.Node_Info
   ) extends Build_Job {
     private val store = build_context.store

 
         val output_shasum = {
           val heap = store.output_heap(session_name)
           if (process_result.ok && store_heap && heap.is_file) {
             val slice = Space.MiB(options.real("build_database_slice")).bytes
-            val digest =
-              using_optional(store.maybe_open_database_server())(
-                ML_Heap.store(_, session_name, heap, slice))
+            val digest = ML_Heap.store(database_server, session_name, heap, slice)
             SHA1.shasum(digest, session_name)
           }
           else SHA1.no_shasum
         }