# HG changeset patch # User wenzelm # Date 1691673081 -7200 # Node ID 5e59f6a46b2f54fd0593038c7f472218713b5a06 # Parent ef03cc736d31b449cc1215e6fe4b02b7d575cdd1 more informative shasum: show differences explicitly; diff -r ef03cc736d31 -r 5e59f6a46b2f src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Aug 10 12:26:20 2023 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Aug 10 15:11:21 2023 +0200 @@ -532,13 +532,25 @@ /* cumulative session info */ - val BUILD_PREFS = "" + private val BUILD_PREFS_BG = "= 0 && { + val s1 = s.substring(i) + s1.startsWith(BUILD_PREFS_BG) && s1.endsWith(BUILD_PREFS_EN) + } + } 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)) + shasum.filter(s => !is_build_prefs(s)) trim(shasum1) == trim(shasum2) } @@ -577,8 +589,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 build_prefs_digests = + session_options.changed(defaults = options0, filter = _.session_content) + .map(ch => SHA1.digest(ch.print_prefs) -> make_build_prefs(ch.name)) val theories = entry.theories.map({ case (opts, thys) => @@ -617,8 +630,7 @@ 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) + SHA1.shasum_meta_info(meta_digest) ::: SHA1.shasum_sorted(build_prefs_digests) val chapter_groups = chapter_defs(chapter).groups val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains)