clarified meta_digest;
authorwenzelm
Wed Oct 11 20:55:11 2017 +0200 (19 months ago)
changeset 66843be08a7691c62
parent 66842 7ded55dd2a55
child 66844 0746d4781674
clarified meta_digest;
NEWS
src/Pure/Thy/sessions.scala
     1.1 --- a/NEWS	Wed Oct 11 20:46:38 2017 +0200
     1.2 +++ b/NEWS	Wed Oct 11 20:55:11 2017 +0200
     1.3 @@ -71,6 +71,10 @@
     1.4    - option -S: only observe changes of sources, not heap images
     1.5    - option -f: forces a fresh build
     1.6  
     1.7 +* Command-line tool "isabelle build" takes "condition" options with the
     1.8 +corresponding environment values into account, when determining the
     1.9 +up-to-date status of a session.
    1.10 +
    1.11  
    1.12  New in Isabelle2017 (October 2017)
    1.13  ----------------------------------
     2.1 --- a/src/Pure/Thy/sessions.scala	Wed Oct 11 20:46:38 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Oct 11 20:55:11 2017 +0200
     2.3 @@ -666,12 +666,16 @@
     2.4              else thy_name
     2.5            }
     2.6  
     2.7 +        val conditions =
     2.8 +          theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
     2.9 +            map(x => (x, Isabelle_System.getenv(x) != ""))
    2.10 +
    2.11          val document_files =
    2.12            entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    2.13  
    2.14          val meta_digest =
    2.15            SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
    2.16 -            entry.theories_no_position, entry.document_files).toString)
    2.17 +            entry.theories_no_position, conditions, entry.document_files).toString)
    2.18  
    2.19          val info =
    2.20            Info(name, entry_chapter, select, entry.pos, entry.groups,