tuned;
authorwenzelm
Wed, 21 Jun 2023 11:05:20 +0200
changeset 78184 4309bcc8f28b
parent 78183 8d57ed9e27a7
child 78185 26b9b40ec1af
tuned;
src/Pure/Thy/store.scala
src/Pure/Tools/build_job.scala
--- 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)