# HG changeset patch
# User wenzelm
# Date 1457465081 -3600
# Node ID 2e352f63d15fb24552ca8d4c97745c859a6dd126
# Parent  905a5db3932df9133e569ff85d3c34497987cd86
separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";

diff -r 905a5db3932d -r 2e352f63d15f src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Tue Mar 08 20:02:46 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML	Tue Mar 08 20:24:41 2016 +0100
@@ -16,9 +16,7 @@
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
         Options.set_default options;
-        Future.ML_statistics := Options.bool options "ML_statistics";
-        Multithreading.trace := Options.int options "threads_trace";
-        Multithreading.max_threads_update (Options.int options "threads");
+        Isabelle_Process.init_options ();
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
       end);
 
diff -r 905a5db3932d -r 2e352f63d15f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Mar 08 20:02:46 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Mar 08 20:24:41 2016 +0100
@@ -11,6 +11,7 @@
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
   val init: string -> unit
+  val init_options: unit -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -203,5 +204,13 @@
     val _ = loop channel;
   in Message_Channel.shutdown msg_channel end);
 
+
+(* init options *)
+
+fun init_options () =
+ (Future.ML_statistics := Options.default_bool "ML_statistics";
+  Multithreading.trace := Options.default_int "threads_trace";
+  Multithreading.max_threads_update (Options.default_int "threads");
+  Goal.parallel_proofs := Options.default_int "parallel_proofs");
+
 end;
-
diff -r 905a5db3932d -r 2e352f63d15f src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Tue Mar 08 20:02:46 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Tue Mar 08 20:24:41 2016 +0100
@@ -72,7 +72,7 @@
     val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
 
     val eval_process =
-      if (process_socket == "") Nil
+      if (process_socket == "") List("Isabelle_Process.init_options ()")
       else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
 
     // bash