# HG changeset patch
# User wenzelm
# Date 1713381631 -7200
# Node ID 2fe244c4bb010d125bd0eae681791204ee2a1d4d
# Parent  39f9084a9668d8e4238f28fb2fabef91801cf741
clarified signature;

diff -r 39f9084a9668 -r 2fe244c4bb01 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/build.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -210,11 +210,9 @@
                 case Some(db) =>
                   using(db)(store.read_build(_, name)) match {
                     case Some(build) if build.ok =>
-                      val session_options = deps0.sessions_structure(name).options
-                      val session_sources = deps0.sources_shasum(name)
-                      if (Sessions.eq_sources(session_options, build.sources, session_sources)) {
-                        None
-                      }
+                      val sources_shasum = deps0.sources_shasum(name)
+                      val thorough = deps0.sessions_structure(name).build_thorough
+                      if (Sessions.eq_sources(thorough, build.sources, sources_shasum)) None
                       else Some(name)
                     case _ => Some(name)
                   }
diff -r 39f9084a9668 -r 2fe244c4bb01 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/build_benchmark.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -67,9 +67,9 @@
 
         def get_shasum(name: String): SHA1.Shasum =
           store.check_output(database_server, name,
-            session_options = build_context.sessions_structure(name).options,
             sources_shasum = sessions(name).sources_shasum,
-            input_shasum = ML_Process.make_shasum(sessions(name).ancestors.map(get_shasum)))._2
+            input_shasum = ML_Process.make_shasum(sessions(name).ancestors.map(get_shasum)),
+            build_thorough = build_context.sessions_structure(name).build_thorough)._2
 
         val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
         val background = deps.background(benchmark_session_name)
diff -r 39f9084a9668 -r 2fe244c4bb01 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/build_process.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -1167,9 +1167,9 @@
     val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
     val (current, output_shasum) =
       store.check_output(_database_server, session_name,
-        session_options = build_context.sessions_structure(session_name).options,
         sources_shasum = sources_shasum,
         input_shasum = input_shasum,
+        build_thorough = build_context.sessions_structure(session_name).build_thorough,
         fresh_build = build_context.fresh_build,
         store_heap = store_heap)
 
diff -r 39f9084a9668 -r 2fe244c4bb01 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -1120,9 +1120,9 @@
         case Some(ancestor_results) if ancestor_results.forall(_.current) =>
           store.check_output(
             _database_server, session_name,
-            session_options = build_context.sessions_structure(session_name).options,
             sources_shasum = state.sessions(session_name).sources_shasum,
             input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum)),
+            build_thorough = build_context.sessions_structure(session_name).build_thorough,
             fresh_build = build_context.fresh_build,
             store_heap = build_context.store_heap || state.sessions.store_heap(session_name))._1
         case _ => false
diff -r 39f9084a9668 -r 2fe244c4bb01 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/sessions.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -577,8 +577,8 @@
     }
   }
 
-  def eq_sources(options: Options, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
-    if (options.bool("build_thorough")) shasum1 == shasum2
+  def eq_sources(thorough: Boolean, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
+    if (thorough) shasum1 == shasum2
     else {
       def trim(shasum: SHA1.Shasum): SHA1.Shasum =
         shasum.filter(s => !is_build_prefs(s))
@@ -721,6 +721,8 @@
     def main_group: Boolean = groups.contains("main")
     def doc_group: Boolean = groups.contains("doc")
 
+    def build_thorough: Boolean = options.bool("build_thorough")
+
     def timeout_ignored: Boolean =
       !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
 
diff -r 39f9084a9668 -r 2fe244c4bb01 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/store.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -485,9 +485,9 @@
   def check_output(
     database_server: Option[SQL.Database],
     name: String,
-    session_options: Options,
     sources_shasum: SHA1.Shasum,
     input_shasum: SHA1.Shasum,
+    build_thorough: Boolean = false,
     fresh_build: Boolean = false,
     store_heap: Boolean = false
   ): (Boolean, SHA1.Shasum) = {
@@ -500,7 +500,7 @@
           val current =
             !fresh_build &&
               build.ok &&
-              Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
+              Sessions.eq_sources(build_thorough, build.sources, sources_shasum) &&
               build.input_heaps == input_shasum &&
               build.output_heap == output_shasum &&
               !(store_heap && output_shasum.is_empty)