# HG changeset patch
# User wenzelm
# Date 1458998063 -3600
# Node ID 63888e5f668b4b6c2fbc7686889210f49c942b11
# Parent  c18a68a3a1f1122ba9c66637985b455694384d0f
clarified use of options;

diff -r c18a68a3a1f1 -r 63888e5f668b src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Mar 26 13:41:14 2016 +0100
+++ b/src/Pure/Tools/build.ML	Sat Mar 26 14:14:23 2016 +0100
@@ -104,17 +104,14 @@
   in
     if null conds then
       (Options.set_default options;
+        Isabelle_Process.init_options ();
         (Thy_Info.use_theories {
           document = Present.document_enabled (Options.string options "document"),
           symbols = symbols,
           last_timing = last_timing,
           master_dir = master_dir}
         |> Unsynchronized.setmp print_mode
-            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
-        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
-        |> Multithreading.max_threads_setmp (Options.int options "threads")
-        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
-        |> Unsynchronized.setmp Future.ML_statistics true) thys)
+            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
     else
       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
         " (undefined " ^ commas conds ^ ")\n")
diff -r c18a68a3a1f1 -r 63888e5f668b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Mar 26 13:41:14 2016 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 26 14:14:23 2016 +0100
@@ -447,7 +447,8 @@
   {
     /* session tree and dependencies */
 
-    val full_tree = Sessions.load(options.int("completion_limit") = 0, dirs, select_dirs)
+    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
+    val full_tree = Sessions.load(build_options, dirs, select_dirs)
     val (selected, selected_tree) =
       full_tree.selection(requirements, all_sessions,
         exclude_session_groups, exclude_sessions, session_groups, sessions)