src/Pure/System/isabelle_process.ML
changeset 52786 9795ea654905
parent 52770 8c7cf864e270
child 52787 c143ad7811fc
     1.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 30 11:44:06 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 30 11:54:57 2013 +0200
     1.3 @@ -3,14 +3,6 @@
     1.4  
     1.5  Isabelle process wrapper, based on private fifos for maximum
     1.6  robustness and performance, or local socket for maximum portability.
     1.7 -
     1.8 -Startup phases:
     1.9 -  - raw Posix process startup with uncontrolled output on stdout/stderr
    1.10 -  - stderr \002: ML running
    1.11 -  - stdin/stdout/stderr freely available (raw ML loop)
    1.12 -  - protocol thread initialization
    1.13 -  - rendezvous on system channel
    1.14 -  - message INIT: channels ready
    1.15  *)
    1.16  
    1.17  signature ISABELLE_PROCESS =
    1.18 @@ -221,19 +213,5 @@
    1.19  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
    1.20  fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
    1.21  
    1.22 -
    1.23 -(* options *)
    1.24 -
    1.25 -val _ =
    1.26 -  protocol_command "Isabelle_Process.options"
    1.27 -    (fn [options_yxml] =>
    1.28 -      let val options = Options.decode (YXML.parse_body options_yxml) in
    1.29 -        Options.set_default options;
    1.30 -        Future.ML_statistics := true;
    1.31 -        Multithreading.trace := Options.int options "threads_trace";
    1.32 -        Multithreading.max_threads := Options.int options "threads";
    1.33 -        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
    1.34 -      end);
    1.35 -
    1.36  end;
    1.37