src/Pure/Tools/build.ML
changeset 59364 3b5da177ae6b
parent 59362 41f1645a4f63
child 59366 e94df7f6b608
     1.1 --- a/src/Pure/Tools/build.ML	Wed Jan 14 11:52:08 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Wed Jan 14 14:28:52 2015 +0100
     1.3 @@ -97,17 +97,6 @@
     1.4  
     1.5  (* build *)
     1.6  
     1.7 -fun use_theories last_timing master_dir (options, thys) =
     1.8 -  let val condition = space_explode "," (Options.string options "condition") in
     1.9 -    (case filter_out (can getenv_strict) condition of
    1.10 -      [] =>
    1.11 -        Thy_Info.use_thys_options last_timing master_dir options
    1.12 -          (map (rpair Position.none) thys)
    1.13 -    | conds =>
    1.14 -        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    1.15 -          " (undefined " ^ commas conds ^ ")\n"))
    1.16 -  end;
    1.17 -
    1.18  fun build args_file = Command_Line.tool0 (fn () =>
    1.19      let
    1.20        val _ = SHA1_Samples.test ();
    1.21 @@ -118,7 +107,7 @@
    1.22            let open XML.Decode in
    1.23              pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    1.24                (pair (list (pair string string)) (pair string (pair string (pair string
    1.25 -                ((list (pair Options.decode (list string))))))))))))
    1.26 +                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
    1.27            end;
    1.28  
    1.29        val _ = Options.set_default options;
    1.30 @@ -140,7 +129,7 @@
    1.31  
    1.32        val res1 =
    1.33          theories |>
    1.34 -          (List.app (use_theories last_timing Path.current)
    1.35 +          (List.app (Thy_Info.build_theories last_timing Path.current)
    1.36              |> session_timing name verbose
    1.37              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    1.38              |> Multithreading.max_threads_setmp (Options.int options "threads")