clarified meta_digest;
authorwenzelm
Wed, 11 Oct 2017 20:55:11 +0200
changeset 66843 be08a7691c62
parent 66842 7ded55dd2a55
child 66844 0746d4781674
clarified meta_digest;
NEWS
src/Pure/Thy/sessions.scala
--- a/NEWS	Wed Oct 11 20:46:38 2017 +0200
+++ b/NEWS	Wed Oct 11 20:55:11 2017 +0200
@@ -71,6 +71,10 @@
   - option -S: only observe changes of sources, not heap images
   - option -f: forces a fresh build
 
+* Command-line tool "isabelle build" takes "condition" options with the
+corresponding environment values into account, when determining the
+up-to-date status of a session.
+
 
 New in Isabelle2017 (October 2017)
 ----------------------------------
--- a/src/Pure/Thy/sessions.scala	Wed Oct 11 20:46:38 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Oct 11 20:55:11 2017 +0200
@@ -666,12 +666,16 @@
             else thy_name
           }
 
+        val conditions =
+          theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
+            map(x => (x, Isabelle_System.getenv(x) != ""))
+
         val document_files =
           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_no_position, entry.document_files).toString)
+            entry.theories_no_position, conditions, entry.document_files).toString)
 
         val info =
           Info(name, entry_chapter, select, entry.pos, entry.groups,