clarified modules (again);
clarified signature: idempotent "finish" operation, analogous to "join";

--- a/src/Pure/Tools/build_job.scala	Mon Feb 13 12:26:24 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Feb 13 12:36:49 2023 +0100
@@ -582,4 +582,12 @@
     else if (result.interrupted) result.error(Output.error_message_text("Interrupt"))
     else result
   }
+
+  lazy val finish: SHA1.Shasum = {
+    require(is_finished, "Build job not finished: " + quote(session_name))
+    if (join.ok && do_store && store.output_heap(session_name).is_file) {
+      SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
+    }
+    else SHA1.no_shasum
+  }
 }

--- a/src/Pure/Tools/build_process.scala	Mon Feb 13 12:26:24 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 12:36:49 2023 +0100
@@ -220,12 +220,7 @@
 
   private def finish_job(session_name: String, job: Build_Job): Unit = {
     val process_result = job.join
-
-    val output_heap =
-      if (process_result.ok && job.do_store && store.output_heap(session_name).is_file) {
-        SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
-      }
-      else SHA1.no_shasum
+    val output_heap = job.finish
 
     val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
     val process_result_tail = {