# 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,