# HG changeset patch
# User wenzelm
# Date 1677751915 -3600
# Node ID 5af7e8ffcab7e46e21f0655312297912feb81c35
# Parent  ed292479eaa9858bdc5cbeccc0040be8dba5dfe5
clarified modules;

diff -r ed292479eaa9 -r 5af7e8ffcab7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 01 22:22:24 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 02 11:11:55 2023 +0100
@@ -1508,6 +1508,32 @@
       (relevant, ok)
     }
 
+    def check_output(
+      name: String,
+      sources_shasum: SHA1.Shasum,
+      input_shasum: SHA1.Shasum,
+      fresh_build: Boolean,
+      store_heap: Boolean
+    ): (Boolean, SHA1.Shasum) = {
+      try_open_database(name) match {
+        case Some(db) =>
+          using(db)(read_build(_, name)) match {
+            case Some(build) =>
+              val output_shasum = find_heap_shasum(name)
+              val current =
+                !fresh_build &&
+                build.ok &&
+                build.sources == sources_shasum &&
+                build.input_heaps == input_shasum &&
+                build.output_heap == output_shasum &&
+                !(store_heap && output_shasum.is_empty)
+              (current, output_shasum)
+            case None => (false, SHA1.no_shasum)
+          }
+        case None => (false, SHA1.no_shasum)
+      }
+    }
+
 
     /* SQL database content */
 
diff -r ed292479eaa9 -r 5af7e8ffcab7 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 22:22:24 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 11:11:55 2023 +0100
@@ -564,25 +564,14 @@
       else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
 
     val store_heap = build_context.store_heap(session_name)
-    val (current, output_shasum) = {
-      store.try_open_database(session_name) match {
-        case Some(db) =>
-          using(db)(store.read_build(_, session_name)) match {
-            case Some(build) =>
-              val output_shasum = store.find_heap_shasum(session_name)
-              val current =
-                !build_context.fresh_build &&
-                build.ok &&
-                build.sources == build_context.sources_shasum(session_name) &&
-                build.input_heaps == input_shasum &&
-                build.output_heap == output_shasum &&
-                !(store_heap && output_shasum.is_empty)
-              (current, output_shasum)
-            case None => (false, SHA1.no_shasum)
-          }
-        case None => (false, SHA1.no_shasum)
-      }
-    }
+
+    val (current, output_shasum) =
+      store.check_output(session_name,
+        sources_shasum = build_context.sources_shasum(session_name),
+        input_shasum = input_shasum,
+        fresh_build = build_context.fresh_build,
+        store_heap = store_heap)
+
     val all_current = current && ancestor_results.forall(_.current)
 
     if (all_current) {