--- a/src/Pure/Thy/store.scala Tue Jun 20 22:57:34 2023 +0200
+++ b/src/Pure/Thy/store.scala Wed Jun 21 11:05:20 2023 +0200
@@ -267,7 +267,10 @@
else SQLite.open_database(path, restrict = true)
def maybe_open_build_database(path: Path): Option[SQL.Database] =
- if (!build_database_test) None else Some(open_build_database(path))
+ if (build_database_test) Some(open_build_database(path)) else None
+
+ def maybe_open_heaps_database(): Option[SQL.Database] =
+ if (build_database_test && build_database_server) Some(open_database_server()) else None
def try_open_database(
name: String,
--- a/src/Pure/Tools/build_job.scala Tue Jun 20 22:57:34 2023 +0200
+++ b/src/Pure/Tools/build_job.scala Wed Jun 21 11:05:20 2023 +0200
@@ -449,19 +449,15 @@
/* output heap */
- val output_shasum =
- if (process_result.ok && store_heap && store.output_heap(session_name).is_file) {
- val database =
- if (store.build_database_test && store.build_database_server) {
- Some(store.open_database_server())
- }
- else None
- val digest =
- try { ML_Heap.write_digest(database, store.output_heap(session_name)) }
- finally { database.foreach(_.close()) }
- SHA1.shasum(digest, session_name)
+ val output_shasum = {
+ val heap = store.output_heap(session_name)
+ if (process_result.ok && store_heap && heap.is_file) {
+ val database = store.maybe_open_heaps_database()
+ try { SHA1.shasum(ML_Heap.write_digest(database, heap), session_name) }
+ finally { database.foreach(_.close()) }
}
else SHA1.no_shasum
+ }
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)