# HG changeset patch
# User wenzelm
# Date 1678785405 -3600
# Node ID e79a5ce8a74c4f5c9b1cb80dbd577fd4492391c6
# Parent  c14db5d674001e0f5668d7e1ce1dd01e7d568d45
clarified modules;

diff -r c14db5d67400 -r e79a5ce8a74c src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Mar 14 10:05:57 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Mar 14 10:16:45 2023 +0100
@@ -11,7 +11,6 @@
 
 
 trait Build_Job {
-  def job_name: String
   def node_info: Host.Node_Info
   def cancel(): Unit = ()
   def is_finished: Boolean = false
@@ -26,8 +25,6 @@
 
   /* build session */
 
-  def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
-
   def start_session(
     build_context: Build_Process.Context,
     progress: Progress,
@@ -111,7 +108,6 @@
     private val store = build_context.store
 
     def session_name: String = session_background.session_name
-    def job_name: String = session_name
 
     private val info: Sessions.Info = session_background.sessions_structure(session_name)
     private val options: Options = node_info.process_policy(info.options)
diff -r c14db5d67400 -r e79a5ce8a74c src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 10:05:57 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 10:16:45 2023 +0100
@@ -248,10 +248,10 @@
     def stop_running(): Unit =
       for (job <- running.valuesIterator; build <- job.build) build.cancel()
 
-    def finished_running(): List[Build_Job] =
+    def finished_running(): List[(String, Build_Job)] =
       List.from(
         for (job <- running.valuesIterator; build <- job.build if build.is_finished)
-        yield build)
+        yield job.name -> build)
 
     def add_running(job: Job): State =
       copy(running = running + (job.name -> job))
@@ -993,6 +993,8 @@
 
   /* build process roles */
 
+  final def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
+
   final def start_build(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
@@ -1038,7 +1040,7 @@
     def start_job(): Boolean = synchronized_database {
       next_job(_state) match {
         case Some(name) =>
-          if (Build_Job.is_session_name(name)) {
+          if (is_session_name(name)) {
             _state = start_session(_state, name)
             true
           }
@@ -1064,8 +1066,7 @@
           synchronized_database {
             if (progress.stopped) _state.stop_running()
 
-            for (build <- _state.finished_running()) {
-              val job_name = build.job_name
+            for ((job_name, build) <- _state.finished_running()) {
               val (process_result, output_shasum) = build.join
               _state = _state.
                 remove_pending(job_name).