# HG changeset patch
# User wenzelm
# Date 1489836296 -3600
# Node ID c262653a3b88b46b268279d880b101011b3fbd49
# Parent  6b840c704441072752d4e4be7ec06b64bca6b091
clarified signature;

diff -r 6b840c704441 -r c262653a3b88 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Mar 17 23:24:04 2017 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sat Mar 18 12:24:56 2017 +0100
@@ -14,7 +14,8 @@
 val _ =
   Isabelle_Process.protocol_command "Prover.options"
     (fn [options_yxml] =>
-      Isabelle_Process.init_protocol_options (Options.decode (YXML.parse_body options_yxml)));
+      (Options.set_default (Options.decode (YXML.parse_body options_yxml));
+       Isabelle_Process.init_options_interactive ()));
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_blob"
diff -r 6b840c704441 -r c262653a3b88 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Mar 17 23:24:04 2017 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Mar 18 12:24:56 2017 +0100
@@ -12,7 +12,7 @@
   val crashes: exn list Synchronized.var
   val init_protocol: string -> unit
   val init_options: unit -> unit
-  val init_protocol_options: Options.T -> unit
+  val init_options_interactive: unit -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -217,9 +217,8 @@
   Multithreading.max_threads_update (Options.default_int "threads");
   Goal.parallel_proofs := Options.default_int "parallel_proofs");
 
-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));
+fun init_options_interactive () =
+ (init_options ();
+  Goal.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0));
 
 end;