# HG changeset patch
# User wenzelm
# Date 1343121277 -7200
# Node ID a25daffda9660d09e4b161d0b0fbcfadb3eb3263
# Parent  a7bf1587eba0b8cf1076b46aa784036311abc33b
observe "condition";

diff -r a7bf1587eba0 -r a25daffda966 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 11:04:49 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 11:14:37 2012 +0200
@@ -12,7 +12,9 @@
 structure Build: BUILD =
 struct
 
-fun use_theories options =
+local
+
+fun use_thys options =
   Thy_Info.use_thys
     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
     |> Unsynchronized.setmp print_mode
@@ -25,6 +27,17 @@
     |> Options.bool options "no_document" ? Present.no_document
     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
 
+fun use_theories (options, thys) =
+  let val condition = space_explode "," (Options.string options "condition") in
+    (case filter_out (can getenv_strict) condition of
+      [] => use_thys options thys
+    | conds =>
+        Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
+          " (missing " ^ commas conds ^ ")\n"))
+  end;
+
+in
+
 fun build args_file =
   let
     val (save, (options, (timing, (verbose, (browser_info, (parent,
@@ -47,7 +60,7 @@
         (Options.string options "browser_info_remote")
         verbose;
 
-    val _ = Session.with_timing name timing (List.app (uncurry use_theories)) theories;
+    val _ = Session.with_timing name timing (List.app use_theories) theories;
     val _ = Session.finish ();
 
     val _ = if save then () else quit ();
@@ -55,3 +68,5 @@
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
 
 end;
+
+end;