more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;

--- a/NEWS	Thu Mar 16 13:18:25 2023 +0100
+++ b/NEWS	Thu Mar 16 15:16:17 2023 +0100
@@ -271,13 +271,16 @@
 
 *** System ***
 
-* Session builds observe dependency of options that contribute to the
-formal content. This is determined via option tags specified in
-etc/options, notably "content" or "document". A change of relavant
-session options causes a fresh build. For example:
-
-  isabelle build -o show_types FOL
+* System option "build_through" determines if session builds should
+observe dependency of options that contribute to the formal content.
+This is specified via option tags given in etc/options (e.g. see
+"isabelle options -l -t content,document"). A change of such options
+causes a fresh build. For example:
+
   isabelle build FOL
+  isabelle build -o show_types FOL  # unchanged, no depency on options
+  isabelle build -o build_thorough -o show_types FOL  # changed
+  isabelle build -o build_thorough FOL  # changed
 
 * The command-line tool "isabelle update" is now directly based on
 "isabelle build" instead of "isabelle dump". Thus it has become more

--- a/etc/options	Thu Mar 16 13:18:25 2023 +0100
+++ b/etc/options	Thu Mar 16 15:16:17 2023 +0100
@@ -174,6 +174,9 @@
 
 section "Build Process"
 
+option build_thorough : bool = false
+  -- "observe dependencies on options with tag 'content' or 'document'"
+
 option build_hostname : string = ""
   -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"
 

--- a/src/Pure/General/sha1.scala	Thu Mar 16 13:18:25 2023 +0100
+++ b/src/Pure/General/sha1.scala	Thu Mar 16 15:16:17 2023 +0100
@@ -67,6 +67,8 @@
 
     def :::(other: Shasum): Shasum = new Shasum(other.rep ::: rep)
 
+    def filter(pred: String => Boolean): Shasum = new Shasum(rep.filter(pred))
+
     def digest: Digest = {
       rep match {
         case List(s)

--- a/src/Pure/Thy/sessions.scala	Thu Mar 16 13:18:25 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 16 15:16:17 2023 +0100
@@ -258,6 +258,7 @@
               List(
                 Info.make(
                   Chapter_Defs.empty,
+                  Options.init0(),
                   info.options,
                   augment_options = _ => Nil,
                   dir_selected = false,
@@ -569,7 +570,7 @@
     def get(name: String): Option[Base] = session_bases.get(name)
 
     def sources_shasum(name: String): SHA1.Shasum = {
-      val meta_info = SHA1.shasum_meta_info(sessions_structure(name).meta_digest)
+      val meta_info = sessions_structure(name).meta_info
       val sources =
         SHA1.shasum_sorted(
           for ((path, digest) <- apply(name).all_sources)
@@ -597,6 +598,17 @@
 
   /* cumulative session info */
 
+  val BUILD_PREFS = "<build_prefs>"
+
+  def eq_sources(options: Options, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
+    if (options.bool("build_thorough")) shasum1 == shasum2
+    else {
+      def trim(shasum: SHA1.Shasum): SHA1.Shasum =
+        shasum.filter(s => !s.endsWith(BUILD_PREFS))
+
+      trim(shasum1) == trim(shasum2)
+    }
+
   sealed case class Chapter_Info(
     name: String,
     pos: Position.T,
@@ -608,6 +620,7 @@
   object Info {
     def make(
       chapter_defs: Chapter_Defs,
+      options0: Options,
       options: Options,
       augment_options: String => List[Options.Spec],
       dir_selected: Boolean,
@@ -630,6 +643,9 @@
         val session_prefs =
           session_options.make_prefs(defaults = session_options0, filter = _.session_content)
 
+        val build_prefs =
+          session_options.make_prefs(defaults = options0, filter = _.session_content)
+
         val theories =
           entry.theories.map({ case (opts, thys) =>
             (session_options ++ opts,
@@ -664,9 +680,11 @@
         val meta_digest =
           SHA1.digest(
             (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
-              entry.theories_no_position, conditions, entry.document_theories_no_position,
-              entry.document_files, session_prefs)
-            .toString)
+              entry.theories_no_position, conditions, entry.document_theories_no_position).toString)
+
+        val meta_info =
+          SHA1.shasum_meta_info(meta_digest) :::
+          SHA1.shasum(SHA1.digest(build_prefs), BUILD_PREFS)
 
         val chapter_groups = chapter_defs(chapter).groups
         val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains)
@@ -674,7 +692,7 @@
         Info(name, chapter, dir_selected, entry.pos, groups, session_path,
           entry.parent, entry.description, directories, session_options, session_prefs,
           entry.imports, theories, global_theories, entry.document_theories, document_files,
-          export_files, entry.export_classpath, meta_digest)
+          export_files, entry.export_classpath, meta_info)
       }
       catch {
         case ERROR(msg) =>
@@ -703,7 +721,7 @@
     document_files: List[(Path, Path)],
     export_files: List[(Path, Int, List[String])],
     export_classpath: List[String],
-    meta_digest: SHA1.Digest
+    meta_info: SHA1.Shasum
   ) {
     def deps: List[String] = parent.toList ::: imports
 
@@ -823,8 +841,8 @@
             }
         }
 
-      val session_prefs =
-        options.make_prefs(defaults = Options.init0(), filter = _.session_content)
+      val options0 = Options.init0()
+      val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
 
       val root_infos = {
         var chapter = UNSORTED
@@ -834,7 +852,7 @@
             case entry: Chapter_Entry => chapter = entry.name
             case entry: Session_Entry =>
               root_infos +=
-                Info.make(chapter_defs, options, augment_options,
+                Info.make(chapter_defs, options0, options, augment_options,
                   root.select, root.dir, chapter, entry)
             case _ =>
           }
@@ -1556,6 +1574,7 @@
 
     def check_output(
       name: String,
+      session_options: Options,
       sources_shasum: SHA1.Shasum,
       input_shasum: SHA1.Shasum,
       fresh_build: Boolean,
@@ -1569,7 +1588,7 @@
               val current =
                 !fresh_build &&
                 build.ok &&
-                build.sources == sources_shasum &&
+                Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
                 build.input_heaps == input_shasum &&
                 build.output_heap == output_shasum &&
                 !(store_heap && output_shasum.is_empty)

--- a/src/Pure/Tools/build.scala	Thu Mar 16 13:18:25 2023 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 16 15:16:17 2023 +0100
@@ -126,8 +126,11 @@
             store.try_open_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
-                  case Some(build)
-                  if build.ok && build.sources == deps0.sources_shasum(name) => None
+                  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
+                    else Some(name)
                   case _ => Some(name)
                 }
               case None => Some(name)

--- a/src/Pure/Tools/build_process.scala	Thu Mar 16 13:18:25 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 16 15:16:17 2023 +0100
@@ -1056,6 +1056,7 @@
 
     val (current, output_shasum) =
       store.check_output(session_name,
+        session_options = build_context.sessions_structure(session_name).options,
         sources_shasum = build_context.sources_shasum(session_name),
         input_shasum = input_shasum,
         fresh_build = build_context.fresh_build,