meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
authorwenzelm
Tue Apr 25 21:31:28 2017 +0200 (2017-04-25)
changeset 6558066351f79c295
parent 65579 52eafedaf196
child 65581 baf96277ee76
child 65583 8d53b3bebab4
child 65588 b0d8d97198b3
meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Apr 25 17:10:17 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 25 21:31:28 2017 +0200
     1.3 @@ -502,6 +502,10 @@
     1.4        theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     1.5        files: List[String],
     1.6        document_files: List[(String, String)]) extends Entry
     1.7 +    {
     1.8 +      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
     1.9 +        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    1.10 +    }
    1.11  
    1.12      private val chapter: Parser[Chapter] =
    1.13      {
    1.14 @@ -583,8 +587,8 @@
    1.15              entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.16  
    1.17            val meta_digest =
    1.18 -            SHA1.digest((entry_chapter, name, entry.parent, entry.options,
    1.19 -              entry.imports, entry.theories, entry.files, entry.document_files).toString)
    1.20 +            SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
    1.21 +              entry.theories_no_position, entry.files, entry.document_files).toString)
    1.22  
    1.23            val info =
    1.24              Info(name, entry_chapter, select, entry.pos, entry.groups,