# HG changeset patch # User wenzelm # Date 1676288209 -3600 # Node ID 3f2b1419f5982f9ccb3f9059ac0c6cd0d560fab5 # Parent 4f4a0c9d2d1a7a82fb55d6b7c1b825f36d562426 clarified modules (again); clarified signature: idempotent "finish" operation, analogous to "join"; diff -r 4f4a0c9d2d1a -r 3f2b1419f598 src/Pure/Tools/build_job.scala --- 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 + } } diff -r 4f4a0c9d2d1a -r 3f2b1419f598 src/Pure/Tools/build_process.scala --- 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 = {