src/Pure/Tools/build.ML
changeset 59362 41f1645a4f63
parent 59175 bf465f335e85
child 59364 3b5da177ae6b
     1.1 --- a/src/Pure/Tools/build.ML	Sun Jan 11 21:06:47 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Tue Jan 13 21:46:09 2015 +0100
     1.3 @@ -97,33 +97,17 @@
     1.4  
     1.5  (* build *)
     1.6  
     1.7 -local
     1.8 -
     1.9 -fun use_theories last_timing options =
    1.10 -  Thy_Info.use_theories {
    1.11 -      document = Present.document_enabled (Options.string options "document"),
    1.12 -      last_timing = last_timing,
    1.13 -      master_dir = Path.current}
    1.14 -    |> Unsynchronized.setmp print_mode
    1.15 -        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    1.16 -    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    1.17 -    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.18 -    |> Multithreading.max_threads_setmp (Options.int options "threads")
    1.19 -    |> Unsynchronized.setmp Future.ML_statistics true;
    1.20 -
    1.21 -fun use_theories_condition last_timing (options, thys) =
    1.22 +fun use_theories last_timing master_dir (options, thys) =
    1.23    let val condition = space_explode "," (Options.string options "condition") in
    1.24      (case filter_out (can getenv_strict) condition of
    1.25        [] =>
    1.26 -        (Options.set_default options;
    1.27 -         use_theories last_timing options (map (rpair Position.none) thys))
    1.28 +        Thy_Info.use_thys_options last_timing master_dir options
    1.29 +          (map (rpair Position.none) thys)
    1.30      | conds =>
    1.31          Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    1.32            " (undefined " ^ commas conds ^ ")\n"))
    1.33    end;
    1.34  
    1.35 -in
    1.36 -
    1.37  fun build args_file = Command_Line.tool0 (fn () =>
    1.38      let
    1.39        val _ = SHA1_Samples.test ();
    1.40 @@ -156,7 +140,7 @@
    1.41  
    1.42        val res1 =
    1.43          theories |>
    1.44 -          (List.app (use_theories_condition last_timing)
    1.45 +          (List.app (use_theories last_timing Path.current)
    1.46              |> session_timing name verbose
    1.47              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    1.48              |> Multithreading.max_threads_setmp (Options.int options "threads")
    1.49 @@ -169,5 +153,3 @@
    1.50      in () end);
    1.51  
    1.52  end;
    1.53 -
    1.54 -end;