clarified use of options;
authorwenzelm
Sat Mar 26 14:14:23 2016 +0100 (2016-03-26)
changeset 6271463888e5f668b
parent 62713 c18a68a3a1f1
child 62715 8312e5d8d217
clarified use of options;
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.ML	Sat Mar 26 13:41:14 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Sat Mar 26 14:14:23 2016 +0100
     1.3 @@ -104,17 +104,14 @@
     1.4    in
     1.5      if null conds then
     1.6        (Options.set_default options;
     1.7 +        Isabelle_Process.init_options ();
     1.8          (Thy_Info.use_theories {
     1.9            document = Present.document_enabled (Options.string options "document"),
    1.10            symbols = symbols,
    1.11            last_timing = last_timing,
    1.12            master_dir = master_dir}
    1.13          |> Unsynchronized.setmp print_mode
    1.14 -            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    1.15 -        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    1.16 -        |> Multithreading.max_threads_setmp (Options.int options "threads")
    1.17 -        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.18 -        |> Unsynchronized.setmp Future.ML_statistics true) thys)
    1.19 +            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
    1.20      else
    1.21        Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
    1.22          " (undefined " ^ commas conds ^ ")\n")
     2.1 --- a/src/Pure/Tools/build.scala	Sat Mar 26 13:41:14 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 26 14:14:23 2016 +0100
     2.3 @@ -447,7 +447,8 @@
     2.4    {
     2.5      /* session tree and dependencies */
     2.6  
     2.7 -    val full_tree = Sessions.load(options.int("completion_limit") = 0, dirs, select_dirs)
     2.8 +    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
     2.9 +    val full_tree = Sessions.load(build_options, dirs, select_dirs)
    2.10      val (selected, selected_tree) =
    2.11        full_tree.selection(requirements, all_sessions,
    2.12          exclude_session_groups, exclude_sessions, session_groups, sessions)