separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
--- 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);
--- 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;
-
--- 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