# HG changeset patch
# User wenzelm
# Date 1689502788 -7200
# Node ID cb0a90df4871cb0d8fbfde3c1439255eb0a5c7f1
# Parent  f5cf8e500dee6914399f6dde59db04e6b3701eb9
prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job");

diff -r f5cf8e500dee -r cb0a90df4871 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Jul 16 11:46:53 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Sun Jul 16 12:19:48 2023 +0200
@@ -106,18 +106,20 @@
     node_info: Host.Node_Info,
     store_heap: Boolean
   ) extends Build_Job {
-    private val store = build_context.store
-
     def session_name: String = session_background.session_name
 
-    private val info: Sessions.Info = session_background.sessions_structure(session_name)
-    private val options: Options = node_info.process_policy(info.options)
-
-    private val session_sources =
-      Store.Sources.load(session_background.base, cache = store.cache.compress)
-
     private val future_result: Future[(Process_Result, SHA1.Shasum)] =
       Future.thread("build", uninterruptible = true) {
+        val info = session_background.sessions_structure(session_name)
+        val options = node_info.process_policy(info.options)
+
+        val store = build_context.store
+
+        store.clean_output(database_server, session_name, session_init = true)
+
+        val session_sources =
+          Store.Sources.load(session_background.base, cache = store.cache.compress)
+
         val env =
           Isabelle_System.settings(
             List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
diff -r f5cf8e500dee -r cb0a90df4871 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Jul 16 11:46:53 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 16 12:19:48 2023 +0200
@@ -1015,8 +1015,6 @@
         (if (store_heap) "Building " else "Running ") + session_name +
           if_proper(node_info.numa_node, " on " + node_info) + " ...")
 
-      store.clean_output(_database_server, session_name, session_init = true)
-
       val session = state.sessions(session_name)
 
       val build =