--- 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 */
--- 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) {