# HG changeset patch
# User wenzelm
# Date 1507748111 -7200
# Node ID be08a7691c62f7a6093703ae3a771260b7bbe3ce
# Parent  7ded55dd2a55784e9e18a8599726da96d4f2c265
clarified meta_digest;

diff -r 7ded55dd2a55 -r be08a7691c62 NEWS
--- 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)
 ----------------------------------
diff -r 7ded55dd2a55 -r be08a7691c62 src/Pure/Thy/sessions.scala
--- 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,