1.1 --- a/src/Pure/System/build.ML	Tue Jul 24 11:04:49 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 11:14:37 2012 +0200
     1.3 @@ -12,7 +12,9 @@
     1.4  structure Build: BUILD =
     1.5  struct
     1.6  
     1.7 -fun use_theories options =
     1.8 +local
     1.9 +
    1.10 +fun use_thys options =
    1.11    Thy_Info.use_thys
    1.12      |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    1.13      |> Unsynchronized.setmp print_mode
    1.14 @@ -25,6 +27,17 @@
    1.15      |> Options.bool options "no_document" ? Present.no_document
    1.16      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
    1.17  
    1.18 +fun use_theories (options, thys) =
    1.19 +  let val condition = space_explode "," (Options.string options "condition") in
    1.20 +    (case filter_out (can getenv_strict) condition of
    1.21 +      [] => use_thys options thys
    1.22 +    | conds =>
    1.23 +        Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
    1.24 +          " (missing " ^ commas conds ^ ")\n"))
    1.25 +  end;
    1.26 +
    1.27 +in
    1.28 +
    1.29  fun build args_file =
    1.30    let
    1.31      val (save, (options, (timing, (verbose, (browser_info, (parent,
    1.32 @@ -47,7 +60,7 @@
    1.33          (Options.string options "browser_info_remote")
    1.34          verbose;
    1.35  
    1.36 -    val _ = Session.with_timing name timing (List.app (uncurry use_theories)) theories;
    1.37 +    val _ = Session.with_timing name timing (List.app use_theories) theories;
    1.38      val _ = Session.finish ();
    1.39  
    1.40      val _ = if save then () else quit ();
    1.41 @@ -55,3 +68,5 @@
    1.42    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    1.43  
    1.44  end;
    1.45 +
    1.46 +end;