CoqIDE: ported to spawn

2 files changed, 18 insertions, 18 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 840ba3e4cd..72db18ef03 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -239,8 +239,11 @@ let get_int opt n =
 
 let get_host_port opt s =
   match CString.split ':' s with
-  | [host; port] -> Some (host, int_of_string port)
-  | _ -> prerr_endline ("Error: host:port expected after option "^opt); exit 1
+  | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+  | ["stdfds"] -> Some Spawned.AnonPipe
+  | _ ->
+     prerr_endline ("Error: host:port or stdfds expected after option "^opt);
+     exit 1
 
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
@@ -326,7 +329,6 @@ let parse_args arglist =
     |"-compile-verbose" -> add_compile true (next ())
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
     |"-exclude-dir" -> exclude_search_in_dirname (next ())
-    |"-ideslave-socket" -> Flags.ide_slave_socket := get_host_port opt (next())
     |"-init-file" -> set_rcfile (next ())
     |"-inputstate"|"-is" -> set_inputstate (next ())
     |"-load-ml-object" -> Mltop.dir_ml_load (next ())
@@ -340,6 +342,8 @@ let parse_args arglist =
     |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
     |"-unsafe" -> add_unsafe (next ())
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
+    |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
+    |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
 
     (* Options with zero arg *)
     |"-batch" -> set_batch_mode ()
@@ -415,6 +419,9 @@ let init arglist =
         prerr_endline "See --help for the list of supported options";
         exit 1
       end;
+      (* If we have been spawned by the Spawn module, this has to be done
+       * early since the master waits us to connect back *)
+      Spawned.init_channels ();
       Envars.set_coqlib Errors.error;
       if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ()));
       if !print_config then (Usage.print_config (); exit (exitcode ()));
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 98386c69e3..e93d167207 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -30,22 +30,16 @@ let init_signal_handler () =
 
 (** Redirection of standard output to a printable buffer *)
 
-let orig_stdout = ref stdout
-
-let init_stdout,read_stdout =
+let init_stdout, read_stdout =
   let out_buff = Buffer.create 100 in
   let out_ft = Format.formatter_of_buffer out_buff in
   let deep_out_ft = Format.formatter_of_buffer out_buff in
   let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
   (fun () ->
      flush_all ();
-     orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout);
-     Unix.dup2 Unix.stderr Unix.stdout;
      Pp_control.std_ft := out_ft;
      Pp_control.err_ft := out_ft;
      Pp_control.deep_ft := deep_out_ft;
-     set_binary_mode_out !orig_stdout true;
-     set_binary_mode_in stdin true;
   ),
   (fun () -> Format.pp_print_flush out_ft ();
              let r = Buffer.contents out_buff in
@@ -365,7 +359,7 @@ let eval_call xml_oc log c =
   Serialize.abstract_eval_call handler c
 
 (** Message dispatching.
-    Since coqtop -ideslave -coq-slaves on starts 1 thread per slave, and each
+    Since coqtop -ideslave starts 1 thread per slave, and each
     thread forwards feedback messages from the slave to the GUI on the same
     xml channel, we need mutual exclusion.  The mutex should be per-channel, but
     here we only use 1 channel. *)
@@ -401,13 +395,12 @@ let slave_feeder xml_oc msg =
 let loop () =
   init_signal_handler ();
   catch_break := false;
-  let in_ch, out_ch =
-    match !Flags.ide_slave_socket with
-    | None -> stdin, !orig_stdout
-    | Some(h,p) ->
-        Unix.open_connection (Unix.ADDR_INET(Unix.inet_addr_of_string h,p)) in
+  let in_ch, out_ch = Spawned.get_channels () in
   let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in
-  let xml_ic = Xml_parser.make (Xml_parser.SChannel in_ch) in
+  Spawned.prepare_in_channel_for_thread_friendly_blocking_input in_ch;
+  let in_lb =
+    Lexing.from_function (Spawned.thread_friendly_blocking_input in_ch) in
+  let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
   set_logger (slave_logger xml_oc);
   set_feeder (slave_feeder xml_oc);
@@ -425,7 +418,7 @@ let loop () =
       let () = pr_debug_answer q r in
 (*       pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *)
       print_xml xml_oc (Serialize.of_answer q r);
-      flush !orig_stdout
+      flush out_ch
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->
 	pr_debug "End of input, exiting gracefully.";