# HG changeset patch # User wenzelm # Date 1493148688 -7200 # Node ID 66351f79c295db0335a26311c696e212119cd0cd # Parent 52eafedaf1966b903cb7167332319f19197d5516 meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT; diff -r 52eafedaf196 -r 66351f79c295 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Apr 25 17:10:17 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Apr 25 21:31:28 2017 +0200 @@ -502,6 +502,10 @@ theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], files: List[String], document_files: List[(String, String)]) extends Entry + { + def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = + theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) + } private val chapter: Parser[Chapter] = { @@ -583,8 +587,8 @@ entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) val meta_digest = - SHA1.digest((entry_chapter, name, entry.parent, entry.options, - entry.imports, entry.theories, entry.files, entry.document_files).toString) + SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports, + entry.theories_no_position, entry.files, entry.document_files).toString) val info = Info(name, entry_chapter, select, entry.pos, entry.groups,