tuned signature;
authorwenzelm
Tue Jul 30 11:54:57 2013 +0200 (2013-07-30 ago)
changeset 527869795ea654905
parent 52785 ecc7d8de4f94
child 52787 c143ad7811fc
tuned signature;
removed notoriously outdated comments;
src/Pure/PIDE/protocol.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/PIDE/protocol.ML	Tue Jul 30 11:44:06 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Jul 30 11:54:57 2013 +0200
     1.3 @@ -8,7 +8,19 @@
     1.4  struct
     1.5  
     1.6  val _ =
     1.7 -  Isabelle_Process.protocol_command "echo" (fn args => List.app writeln args);
     1.8 +  Isabelle_Process.protocol_command "Isabelle_Process.echo"
     1.9 +    (fn args => List.app writeln args);
    1.10 +
    1.11 +val _ =
    1.12 +  Isabelle_Process.protocol_command "Isabelle_Process.options"
    1.13 +    (fn [options_yxml] =>
    1.14 +      let val options = Options.decode (YXML.parse_body options_yxml) in
    1.15 +        Options.set_default options;
    1.16 +        Future.ML_statistics := true;
    1.17 +        Multithreading.trace := Options.int options "threads_trace";
    1.18 +        Multithreading.max_threads := Options.int options "threads";
    1.19 +        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
    1.20 +      end);
    1.21  
    1.22  val _ =
    1.23    Isabelle_Process.protocol_command "Document.define_command"
     2.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 30 11:44:06 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 30 11:54:57 2013 +0200
     2.3 @@ -3,14 +3,6 @@
     2.4  
     2.5  Isabelle process wrapper, based on private fifos for maximum
     2.6  robustness and performance, or local socket for maximum portability.
     2.7 -
     2.8 -Startup phases:
     2.9 -  - raw Posix process startup with uncontrolled output on stdout/stderr
    2.10 -  - stderr \002: ML running
    2.11 -  - stdin/stdout/stderr freely available (raw ML loop)
    2.12 -  - protocol thread initialization
    2.13 -  - rendezvous on system channel
    2.14 -  - message INIT: channels ready
    2.15  *)
    2.16  
    2.17  signature ISABELLE_PROCESS =
    2.18 @@ -221,19 +213,5 @@
    2.19  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
    2.20  fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
    2.21  
    2.22 -
    2.23 -(* options *)
    2.24 -
    2.25 -val _ =
    2.26 -  protocol_command "Isabelle_Process.options"
    2.27 -    (fn [options_yxml] =>
    2.28 -      let val options = Options.decode (YXML.parse_body options_yxml) in
    2.29 -        Options.set_default options;
    2.30 -        Future.ML_statistics := true;
    2.31 -        Multithreading.trace := Options.int options "threads_trace";
    2.32 -        Multithreading.max_threads := Options.int options "threads";
    2.33 -        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
    2.34 -      end);
    2.35 -
    2.36  end;
    2.37