src/Pure/Tools/build.ML
changeset 54458 96ccc8972fc7
parent 53212 387b9f7cb0ac
child 54717 42c209a6c225
     1.1 --- a/src/Pure/Tools/build.ML	Sat Nov 16 21:29:18 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Sat Nov 16 22:17:45 2013 +0100
     1.3 @@ -97,18 +97,18 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun no_document options =
     1.8 -  (case Options.string options "document" of "" => true | "false" => true | _ => false);
     1.9 -
    1.10  fun use_theories last_timing options =
    1.11 -  Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    1.12 +  Thy_Info.use_theories {
    1.13 +      document =
    1.14 +        (case Options.string options "document" of "" => false | "false" => false | _ => true),
    1.15 +      last_timing = last_timing,
    1.16 +      master_dir = Path.current}
    1.17      |> Unsynchronized.setmp print_mode
    1.18          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    1.19      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    1.20      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.21      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    1.22      |> Unsynchronized.setmp Future.ML_statistics true
    1.23 -    |> no_document options ? Present.no_document
    1.24      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    1.25      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    1.26