--- 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)