Fix CoqIDE on windows

10 files changed, 99 insertions, 24 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 5d8efebd1..8442493b4 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -327,7 +327,7 @@ let lift (f : unit -> 'a) : 'a task =
     closed in coqide.
 *)
 
-let open_process_pid prog args =
+let open_coqtop_pipe prog args =
   let (ide2top_r,ide2top_w) = Unix.pipe () in
   let (top2ide_r,top2ide_w) = Unix.pipe () in
   Unix.set_close_on_exec ide2top_w;
@@ -343,6 +343,34 @@ let open_process_pid prog args =
   Unix.out_channel_of_descr ide2top_w,
   (fun () -> Unix.close top2ide_r; Unix.close ide2top_w)
 
+let open_coqtop_socket prog args =
+  let s = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in
+  Unix.bind s (Unix.ADDR_INET (Unix.inet_addr_loopback,0));
+  Unix.listen s 1;
+  let host, port =
+    match Unix.getsockname s with
+    | Unix.ADDR_INET(host, port) ->
+        Unix.string_of_inet_addr host, string_of_int port
+    | _ -> assert false in
+  let pid =
+    Unix.create_process prog
+      (Array.append args [|"-ideslave-socket";host^":"^port|])
+      (Unix.openfile "slave.in"  [Unix.O_CREAT;Unix.O_RDONLY] 0o660)
+      (Unix.openfile "slave.out" [Unix.O_CREAT;Unix.O_WRONLY] 0o660)
+      (Unix.openfile "slave.err" [Unix.O_CREAT;Unix.O_WRONLY] 0o660) in
+  assert (pid <> 0);
+  let cs, _ = Unix.accept s in
+  Unix.set_nonblock cs;
+  pid, 
+  Unix.in_channel_of_descr cs, 
+  Glib.Io.channel_of_descr_socket cs,
+  Unix.out_channel_of_descr cs,
+  (fun () -> Unix.close cs; Unix.close s)
+
+let open_process_pid prog args =
+  if Sys.os_type = "Unix" then open_coqtop_pipe prog args
+  else open_coqtop_socket prog args
+
 exception TubeError
 exception AnswerWithoutRequest of string
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5b2ca6f8b..b223be3a4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -171,7 +171,7 @@ let check_quit saveall =
                 "Quit without Saving";
                 "Don't Quit"]
       ~default:0
-      ~icon:warn_image#coerce
+      ~icon:(warn_image ())#coerce
       "There are unsaved buffers"
     in
     match answ with
@@ -259,7 +259,7 @@ let close_buffer sn =
                 "Close without Saving";
                 "Don't Close"]
       ~default:0
-      ~icon:warn_image#coerce
+      ~icon:(warn_image ())#coerce
       "This buffer has unsaved modifications"
     in
     match answ with
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
index a1066db2c..3b8599818 100644
--- a/ide/fileOps.ml
+++ b/ide/fileOps.ml
@@ -108,7 +108,7 @@ object(self)
     let answ = GToolbox.question_box ~title:"File exists on disk"
       ~buttons:["Overwrite"; "Cancel";]
       ~default:1
-      ~icon:warn_image#coerce
+      ~icon:(warn_image ())#coerce
       ("File "^f^" already exists")
     in
     match answ with
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 881f5ea43..2ae46fc7e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -11,14 +11,14 @@ open Preferences
 
 exception Forbidden
 
-let warn_image =
+let warn_image () =
   let img = GMisc.image () in
   img#set_stock `DIALOG_WARNING;
   img#set_icon_size `DIALOG;
   img
 
-let warning msg =
-  GToolbox.message_box ~title:"Warning" ~icon:warn_image#coerce msg
+let warning msg = 
+   GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg 
 
 let cb = GData.clipboard Gdk.Atom.primary
 
@@ -328,7 +328,10 @@ let io_read_all chan =
     let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
     Buffer.add_substring read_buffer read_string 0 len
   in
-  begin try while true do read_once () done with _ -> () end;
+  begin
+    try while true do read_once () done
+    with Glib.GError _ -> ()
+  end;
   Buffer.contents read_buffer
 
 (** Run an external command asynchronously *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index bb9e65322..5fd97e3a5 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val warn_image : GMisc.image
+val warn_image : unit -> GMisc.image
 val warning : string -> unit
 
 val cb : GData.clipboard
diff --git a/lib/flags.ml b/lib/flags.ml
index cde45a81f..b79f80d22 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,7 +45,6 @@ let boot = ref false
 
 let batch_mode = ref false
 
-let ide_slave_mode = ref false
 let coq_slave_mode = ref (-1)
 let coq_slaves_number = ref 1
 
@@ -60,6 +59,7 @@ let term_quality = ref false
 let xml_export = ref false
 
 let ide_slave = ref false
+let ide_slave_socket = ref None
 
 let time = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 8525d731b..0b7adf33f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -12,7 +12,6 @@ val boot : bool ref
 
 val batch_mode : bool ref
 
-val ide_slave_mode : bool ref
 val coq_slave_mode : int ref
 val coq_slaves_number : int ref
 
@@ -27,6 +26,7 @@ val term_quality : bool ref
 val xml_export : bool ref
 
 val ide_slave : bool ref
+val ide_slave_socket : (string * int) option ref
 
 val time : bool ref
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f3bcee128..a0de42bf6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -233,6 +233,11 @@ let get_int opt n =
   with Failure _ ->
     prerr_endline ("Error: integer expected after option "^opt); exit 1
 
+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
+
 let parse_args arglist =
   let args = ref arglist in
   let extras = ref [] in
@@ -272,6 +277,7 @@ 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 ())
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index be384e174..98386c69e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -401,8 +401,13 @@ let slave_feeder xml_oc msg =
 let loop () =
   init_signal_handler ();
   catch_break := false;
-  let xml_oc = Xml_printer.make (Xml_printer.TChannel !orig_stdout) in
-  let xml_ic = Xml_parser.make (Xml_parser.SChannel stdin) in
+  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 xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in
+  let xml_ic = Xml_parser.make (Xml_parser.SChannel in_ch) in
   let () = Xml_parser.check_eof xml_ic false in
   set_logger (slave_logger xml_oc);
   set_feeder (slave_feeder xml_oc);
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index ea9a85f51..5f1c31e42 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -7,9 +7,10 @@
 (************************************************************************)
 
 let prerr_endline s =
-  if !Flags.debug then
-    prerr_endline (Printf.sprintf "%d] %s" !Flags.coq_slave_mode s)
-  else ()
+  if !Flags.debug then begin
+    prerr_endline (Printf.sprintf "%d] %s" !Flags.coq_slave_mode s);
+    flush stderr
+  end else ()
 
 open Vernacexpr
 open Errors
@@ -654,6 +655,16 @@ end = struct (* {{{ *)
       | Some managers -> Array.length managers
     let is_empty () = !slave_managers = None
 
+    let master_handshake ic oc =
+      try
+        Marshal.to_channel oc 17 [];  flush oc;
+        let n = (Marshal.from_channel ic : int) in
+        assert(n = 17);
+        prerr_endline "Handshake OK"
+      with e ->
+        prerr_endline ("Handshake failed: "^Printexc.to_string e);
+        exit 1
+
     let respawn n () =
       let c2s_r, c2s_w = Unix.pipe () in
       let s2c_r, s2c_w = Unix.pipe () in
@@ -674,7 +685,12 @@ end = struct (* {{{ *)
       let pid = Unix.create_process_env prog args env c2s_r s2c_w Unix.stderr in
       Unix.close c2s_r;
       Unix.close s2c_w;
-      Unix.in_channel_of_descr s2c_r, Unix.out_channel_of_descr c2s_w, pid, n
+      let s2c_r = Unix.in_channel_of_descr s2c_r in
+      let c2s_w = Unix.out_channel_of_descr c2s_w in
+      set_binary_mode_out c2s_w true;
+      set_binary_mode_in s2c_r true;
+      master_handshake s2c_r c2s_w;
+      s2c_r, c2s_w, pid, n
 
     let init n manage_slave =
       slave_managers := Some
@@ -763,11 +779,13 @@ end = struct (* {{{ *)
 
   let marshal_request oc (req : request) =
     try marshal_to_channel oc req
-    with Failure s | Invalid_argument s -> marshal_err ("marshal_request: "^s)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("marshal_request: "^s)
 
   let unmarshal_request ic =
     try (Marshal.from_channel ic : request)
-    with Failure s | Invalid_argument s -> marshal_err ("unmarshal_request: "^s)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_request: "^s)
 
   (* Since cancelling is still cooperative, the slave runs a thread that
      periodically sends a RespTick message on the same channel used by the
@@ -778,20 +796,23 @@ end = struct (* {{{ *)
     fun oc (res : response) ->
       Mutex.lock m;
       try marshal_to_channel oc res; Mutex.unlock m
-      with Failure s | Invalid_argument s ->
+      with Failure s | Invalid_argument s | Sys_error s ->
         Mutex.unlock m; marshal_err ("marshal_response: "^s)
   
   let unmarshal_response ic =
     try (Marshal.from_channel ic : response)
-    with Failure s | Invalid_argument s -> marshal_err ("unmarshal_response: "^s)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_response: "^s)
   
   let marshal_more_data oc (res : more_data) =
     try marshal_to_channel oc res
-    with Failure s | Invalid_argument s -> marshal_err ("marshal_more_data: "^s)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("marshal_more_data: "^s)
   
   let unmarshal_more_data ic =
     try (Marshal.from_channel ic : more_data)
-    with Failure s | Invalid_argument s -> marshal_err ("unmarshal_more_data: "^s)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_more_data: "^s)
 
   let queue : task TQueue.t = TQueue.create ()
 
@@ -823,7 +844,8 @@ end = struct (* {{{ *)
   let rec manage_slave respawn =
     let ic, oc, pid, id_slave = respawn () in
     let kill_pid =
-      ref (fun () -> try Unix.kill pid 9 with Unix.Unix_error _ -> ()) in
+      ref (fun () -> try Unix.kill pid 9
+                     with Unix.Unix_error _ | Invalid_argument _ -> ()) in
     at_exit (fun () -> !kill_pid ());
     let last_task = ref None in
     try
@@ -940,6 +962,16 @@ end = struct (* {{{ *)
       | [] -> let data = f () in l := List.tl data; List.hd data
       | x::tl -> l := tl; x
 
+  let slave_handshake () =
+    try
+      let v = (Marshal.from_channel !slave_ic : int) in
+      assert(v = 17);
+      Marshal.to_channel !slave_oc v [];  flush !slave_oc;
+      prerr_endline "Handshake OK"
+    with e ->
+      prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
+      exit 1
+
   let slave_main_loop reset =
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback fb) [];
@@ -959,6 +991,7 @@ end = struct (* {{{ *)
         Unix.sleep n;
         if !working then marshal_response !slave_oc RespTick
       done) 1 in
+    slave_handshake ();
     while true do
       try
         working := false;