Coqide: better handling of stdout/stderr in win32

 Now that coqide is a console-free win32 app, writing to
 nonexistent stdout/stderr lead to Sys_error. To avoid that:

 - We reroute coqide's stdout/stderr to either a pipe that will stay
   unread (by default), or to a temp log file (in debug mode).

 - When doing create_process, avoid referring to Unix.stderr:
   anything printed by coqtop to its stderr will be merged in the
   regular channel.

 - On the coqtop side, remove the awkward fix consisting in a \r printed
   on stderr apparently to fix coqide.byte. This fix is probably obsolete
   since the separation of coqide and coqtop as distinct processes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14047 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 37 insertions, 17 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 064447549..e0b08562b 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -135,17 +135,22 @@ let coqtop_zombies () =
     doesn't call bin/sh, so args shouldn't be quoted. The process
     cannot be terminated by a Unix.close_process, but rather by a
     kill of the pid.
+
+           >--ide2top_w--[pipe]--ide2top_r-->
+    coqide                                   coqtop
+           <--top2ide_r--[pipe]--top2ide_w--<
+
 *)
 
 let open_process_pid prog args =
-  let (in_read,in_write) = Unix.pipe () in
-  let (out_read,out_write) = Unix.pipe () in
-  let pid = Unix.create_process prog args out_read in_write Unix.stderr in
+  let (ide2top_r,ide2top_w) = Unix.pipe () in
+  let (top2ide_r,top2ide_w) = Unix.pipe () in
+  let pid = Unix.create_process prog args ide2top_r top2ide_w top2ide_w in
   assert (pid <> 0);
-  Unix.close out_read;
-  Unix.close in_write;
-  let ic = Unix.in_channel_of_descr in_read in
-  let oc = Unix.out_channel_of_descr out_write in
+  Unix.close ide2top_r;
+  Unix.close top2ide_w;
+  let oc = Unix.out_channel_of_descr ide2top_w in
+  let ic = Unix.in_channel_of_descr top2ide_r in
   set_binary_mode_out oc true;
   set_binary_mode_in ic true;
   (pid,ic,oc)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index ceeaa199d..1987b97ac 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -19,17 +19,36 @@ let initmac () = IFDEF MacInt THEN gtk_mac_init Coqide.do_load Coqide.forbid_qui
 let macready () = IFDEF MacInt THEN gtk_mac_ready () ELSE ()  END
 
 (* On win32, we add the directory of coqide to the PATH at launch-time
-   (this used to be done in a .bat script).
-   We also provide a specific kill function.
+   (this used to be done in a .bat script). *)
+
+let set_win32_path () =
+  Unix.putenv "PATH"
+    (Filename.dirname Sys.executable_name ^ ";" ^
+      (try Sys.getenv "PATH" with _ -> ""))
+
+(* On win32, since coqide is now console-free, we re-route stdout/stderr
+   to avoid Sys_error if someone writes to them. We write to a pipe which
+   is never read (by default) or to a temp log file (when in debug mode).
 *)
 
+let reroute_stdout_stderr () =
+  let out_descr =
+    if !Ideutils.debug then
+      Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log"))
+    else
+      snd (Unix.pipe ())
+  in
+  Unix.dup2 out_descr Unix.stdout;
+  Unix.dup2 out_descr Unix.stderr
+
+(* We also provide a specific kill function. *)
+
 IFDEF Win32 THEN
 external win32_kill : int -> unit = "win32_kill"
 let () =
-  Unix.putenv "PATH"
-    (Filename.dirname Sys.executable_name ^ ";" ^
-      (try Sys.getenv "PATH" with _ -> ""));
-  Coq.killer := win32_kill
+  Coq.killer := win32_kill;
+  set_win32_path ();
+  reroute_stdout_stderr ()
 END
 
 let () =
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index e2d22472a..a39e9c429 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -261,10 +261,6 @@ let interp (verbosely,s) =
   let pa = parsable_of_string s in
   try
     let (loc,vernac) = Vernac.parse_sentence (pa,None) in
-    (* Temporary hack to make coqide.byte work (WTF???) - now with
-     * less screen
-     *   * pollution *)
-    Pervasives.prerr_string " \r"; Pervasives.flush stderr;
     if is_vernac_debug_command vernac then
       user_error_loc loc (str "Debug mode not available within CoqIDE");
     if is_vernac_navigation_command vernac then