src/Pure/System/build.ML
changeset 48470 7483aa690b4f
parent 48468 7f2998b95249
child 48472 6ebb6cdd36a5
equal deleted inserted replaced
48469:826a771cff33 48470:7483aa690b4f
    22     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    22     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    23     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    23     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    24         (Options.int options "parallel_proofs_threshold")
    24         (Options.int options "parallel_proofs_threshold")
    25     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    25     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    26     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    26     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    27     |> Options.bool options "no_document" ? Present.no_document
    27     |> (case Options.string options "document" of "" => false | "false" => false | _ => true) ?
       
    28         Present.no_document
    28     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
    29     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
    29 
    30 
    30 fun use_theories (options, thys) =
    31 fun use_theories (options, thys) =
    31   let val condition = space_explode "," (Options.string options "condition") in
    32   let val condition = space_explode "," (Options.string options "condition") in
    32     (case filter_out (can getenv_strict) condition of
    33     (case filter_out (can getenv_strict) condition of