# HG changeset patch
# User wenzelm
# Date 1692190217 -7200
# Node ID d637e60427db1e03c393935ca0bdf6daab18c7a4
# Parent  0e79fa88cab6f488381a0a629daf029eed74a71d
tuned signature;

diff -r 0e79fa88cab6 -r d637e60427db src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Aug 16 14:42:43 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Aug 16 14:50:17 2023 +0200
@@ -13,10 +13,13 @@
 trait Build_Job {
   def cancel(): Unit = ()
   def is_finished: Boolean = false
-  def join: Option[(Process_Result, SHA1.Shasum)] = None
+  def join: Option[Build_Job.Result] = None
 }
 
 object Build_Job {
+  sealed case class Result(process_result: Process_Result, output_shasum: SHA1.Shasum)
+
+
   /* build session */
 
   def start_session(
@@ -111,7 +114,7 @@
   ) extends Build_Job {
     def session_name: String = session_background.session_name
 
-    private val future_result: Future[Option[(Process_Result, SHA1.Shasum)]] =
+    private val future_result: Future[Option[Result]] =
       Future.thread("build", uninterruptible = true) {
         val info = session_background.sessions_structure(session_name)
         val options = build_context.engine.process_options(info.options, node_info)
@@ -537,12 +540,13 @@
             }
           }
 
-          if (valid) Some((process_result.copy(out_lines = log_lines), output_shasum)) else None
+          if (valid) Some(Result(process_result.copy(out_lines = log_lines), output_shasum))
+          else None
         }
       }
 
     override def cancel(): Unit = future_result.cancel()
     override def is_finished: Boolean = future_result.is_finished
-    override def join: Option[(Process_Result, SHA1.Shasum)] = future_result.join
+    override def join: Option[Result] = future_result.join
   }
 }
diff -r 0e79fa88cab6 -r d637e60427db src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Aug 16 14:42:43 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Aug 16 14:50:17 2023 +0200
@@ -55,7 +55,7 @@
     build: Option[Build_Job]
   ) extends Library.Named {
     def no_build: Job = copy(build = None)
-    def join_build: Option[(Process_Result, SHA1.Shasum)] = build.flatMap(_.join)
+    def join_build: Option[Build_Job.Result] = build.flatMap(_.join)
   }
 
   sealed case class Result(
@@ -1142,12 +1142,14 @@
               job.join_build match {
                 case None =>
                   _state = _state.remove_running(job.name)
-                case Some((process_result, output_shasum)) =>
+                case Some(result) =>
                   val result_name = (job.name, worker_uuid, build_uuid)
                   _state = _state.
                     remove_pending(job.name).
                     remove_running(job.name).
-                    make_result(result_name, process_result, output_shasum,
+                    make_result(result_name,
+                      result.process_result,
+                      result.output_shasum,
                       node_info = job.node_info)
               }
             }