# HG changeset patch
# User wenzelm
# Date 1457810257 -3600
# Node ID f35858c831e54661c05ff2243ad45d5c46091285
# Parent  cf79f8866bc310328e3cb5c811194c360aa87a89
clarified session build options: already provided by ML_Process;
tuned signature;

diff -r cf79f8866bc3 -r f35858c831e5 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sat Mar 12 20:17:37 2016 +0100
@@ -14,11 +14,7 @@
 val _ =
   Isabelle_Process.protocol_command "Prover.options"
     (fn [options_yxml] =>
-      let val options = Options.decode (YXML.parse_body options_yxml) in
-        Options.set_default options;
-        Isabelle_Process.init_options ();
-        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
-      end);
+      Isabelle_Process.init_protocol_options (Options.decode (YXML.parse_body options_yxml)));
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_blob"
diff -r cf79f8866bc3 -r f35858c831e5 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Mar 12 20:17:37 2016 +0100
@@ -12,6 +12,8 @@
   val crashes: exn list Synchronized.var
   val init_protocol: string -> unit
   val init_options: unit -> unit
+  val init_build_options: unit -> unit
+  val init_protocol_options: Options.T -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -213,4 +215,13 @@
   Multithreading.max_threads_update (Options.default_int "threads");
   Goal.parallel_proofs := Options.default_int "parallel_proofs");
 
+fun init_build_options () =
+ (Options.load_default ();
+  init_options ());
+
+fun init_protocol_options options =
+ (Options.set_default options;
+  init_options ();
+  Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0));
+
 end;
diff -r cf79f8866bc3 -r f35858c831e5 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/Pure/Tools/build.ML	Sat Mar 12 20:17:37 2016 +0100
@@ -124,30 +124,30 @@
     let
       val _ = SHA1_Samples.test ();
 
-      val (symbol_codes, (command_timings, (output, (options, (verbose, (browser_info,
-          (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
+      val (symbol_codes, (command_timings, (output, (verbose, (browser_info,
+            (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
         File.read (Path.explode args_file) |> YXML.parse_body |>
           let open XML.Decode in
-            pair (list (pair string int)) (pair (list properties) (pair string (pair Options.decode
+            pair (list (pair string int)) (pair (list properties) (pair string
               (pair bool (pair string (pair (list (pair string string)) (pair string
                 (pair string (pair string (pair string
-                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
+                ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
           end;
       val do_output = output <> "";
 
       val symbols = HTML.make_symbols symbol_codes;
-      val _ = Options.set_default options;
+      val _ = Isabelle_Process.init_build_options ();
 
       val _ = writeln ("\fSession.name = " ^ name);
       val _ =
         Session.init
           symbols
           do_output
-          (Options.bool options "browser_info")
+          (Options.default_bool "browser_info")
           (Path.explode browser_info)
-          (Options.string options "document")
-          (Options.string options "document_output")
-          (Present.document_variants (Options.string options "document_variants"))
+          (Options.default_string "document")
+          (Options.default_string "document_output")
+          (Present.document_variants (Options.default_string "document_variants"))
           (map (apply2 Path.explode) document_files)
           (Path.explode graph_file)
           parent_name (chapter, name)
@@ -160,7 +160,7 @@
           (List.app (build_theories symbols last_timing Path.current)
             |> session_timing name verbose
             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
-            |> Multithreading.max_threads_setmp (Options.int options "threads")
+            |> Multithreading.max_threads_setmp (Options.default_int "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();
       val _ = Par_Exn.release_all [res1, res2];
diff -r cf79f8866bc3 -r f35858c831e5 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Mar 11 17:20:14 2016 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 12 20:17:37 2016 +0100
@@ -549,28 +549,13 @@
     try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
     catch { case ERROR(_) => /*error should be exposed in ML*/ }
 
-    private val args_file = Isabelle_System.tmp_file("args")
-    private val args_standard_path = File.standard_path(args_file)
-    File.write(args_file, YXML.string_of_body(
-      if (is_pure(name)) Options.encode(info.options)
-      else
-        {
-          val theories = info.theories.map(x => (x._2, x._3))
-          import XML.Encode._
-          pair(list(pair(string, int)), pair(list(properties), pair(string, pair(Options.encode,
-            pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
-            pair(string, pair(string, pair(string,
-            list(pair(Options.encode, list(Path.encode))))))))))))))(
-          (Symbol.codes, (command_timings, (output_standard_path, (info.options,
-            (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file),
-            (parent, (info.chapter, (name,
-            theories))))))))))))
-        }))
-
     output.file.delete
 
     private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
 
+    private val args_file =
+      if (is_pure(name)) None else Some(Isabelle_System.tmp_file("args"))
+
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
         val process =
@@ -579,13 +564,26 @@
               "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
               " Session.shutdown (); ML_Heap.share_common_data ();" +
               " ML_Heap.save_state " + ML_Syntax.print_string_raw(output_standard_path) + "));"
-            val env1 = env + ("ISABELLE_PROCESS_OPTIONS" -> args_standard_path)
             ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
-              cwd = info.dir.file, env = env1)
+              cwd = info.dir.file, env = env)
           }
           else {
+            File.write(args_file.get, YXML.string_of_body(
+                {
+                  val theories = info.theories.map(x => (x._2, x._3))
+                  import XML.Encode._
+                  pair(list(pair(string, int)), pair(list(properties), pair(string, pair(bool,
+                    pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
+                    pair(string, pair(string, pair(string,
+                    list(pair(Options.encode, list(Path.encode)))))))))))))(
+                  (Symbol.codes, (command_timings, (output_standard_path, (verbose,
+                    (browser_info, (info.document_files, (File.standard_path(graph_file),
+                    (parent, (info.chapter, (name,
+                    theories)))))))))))
+                }))
             ML_Process(info.options, parent,
-              List("--eval", "Build.build " + ML_Syntax.print_string_raw(args_standard_path)),
+              List("--eval", "Build.build " +
+                ML_Syntax.print_string_raw(File.standard_path(args_file.get))),
               cwd = info.dir.file, env = env)
           }
         process.result(
@@ -621,7 +619,7 @@
         Present.finish(progress, browser_info, graph_file, info, name)
 
       graph_file.delete
-      args_file.delete
+      args_file.foreach(_.delete)
       timeout_request.foreach(_.cancel)
 
       if (result.interrupted) {