Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be used

 This is an adaptation of commit r13751 of branch 8.3

 Even if coqide.exe keeps its console by default for the moment,
 we try to allow turning it off (for instance via the mkwinapp tool) :
 for that we need to be cautious about the use of functions
 like prerr_endline. Since stderr doesn't exists in this settings,
 such functions trigger a Sys_error "bad file descriptor".
 This patch protects many access to std** by a (try ... with _ ->()).

 Nota: with camlp5 < 6.02.1, Print Grammar was also generating
 such a Sys_error.

 TODO: we should try to figure a way of displaying messages (both
  debug and early/late error message). A log file ? A popup ?
  diplay in the response buffer ?

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

5 files changed, 34 insertions, 19 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 3c7ee2de8e..1acea4a9bc 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -8,9 +8,6 @@
 
 open Ideutils
 
-let prerr_endline s = if !debug then prerr_endline s else ()
-
-
 (** * Version and date *)
 
 let get_version_date () =
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 726931cac6..08c41aeaa8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -190,7 +190,7 @@ let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
 
 let crash_save i =
   (*  ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
-  Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
+  safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
   let count = ref 0 in
   List.iter
     (function {script=view; analyzed_view = av } ->
@@ -202,12 +202,12 @@ let crash_save i =
        in
        try
 	 if try_export filename (view#buffer#get_text ()) then
-	   Pervasives.prerr_endline ("Saved "^filename)
-	 else Pervasives.prerr_endline ("Could not save "^filename)
-       with _ -> Pervasives.prerr_endline ("Could not save "^filename))
+	   safe_prerr_endline ("Saved "^filename)
+	 else safe_prerr_endline ("Could not save "^filename)
+       with _ -> safe_prerr_endline ("Could not save "^filename))
     )
     session_notebook#pages;
-  Pervasives.prerr_endline "Done. Please report.";
+  safe_prerr_endline "Done. Please report.";
   if i <> 127 then exit i
 
 let ignore_break () =
@@ -3188,11 +3188,10 @@ let process_argv argv =
   try
     let continue,filtered = Coq.filter_coq_opts (List.tl argv) in
     if not continue then
-      (List.iter Pervasives.prerr_endline filtered; exit 0);
+      (List.iter safe_prerr_endline filtered; exit 0);
     let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
     if opts <> [] then
-      (output_string stderr ("Illegal option: "^List.hd opts^"\n");
-       exit 1);
+      (safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1);
     filtered
   with _ ->
-    (output_string stderr "coqtop choked on one of your option"; exit 1)
+    (safe_prerr_endline "coqtop choked on one of your option"; exit 1)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index c63db00316..9fc0f72b71 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 IFDEF MacInt THEN
 external gtk_mac_init : (string -> unit) -> (unit -> bool) -> unit
   = "caml_gtk_mac_init"
@@ -41,9 +49,9 @@ let () =
       try
 	GtkThread.main ()
       with
-	| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
+	| Sys.Break -> Ideutils.prerr_endline "Interrupted." ; flush stderr
 	| e ->
-	    Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
-	    flush stderr;
+	    Ideutils.safe_prerr_endline
+	      ("CoqIde unexpected error:" ^ (Printexc.to_string e));
 	    Coqide.crash_save 127
     done
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a4126ae33d..faaaa37423 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -31,10 +31,17 @@ let pbar = GRange.progress_bar ~pulse_step:0.2 ()
 
 let debug = Flags.debug
 
+(* On a Win32 application with no console, writing to stderr raise
+   a Sys_error "bad file descriptor", hence the "try" below.
+   Ideally, we should re-route message to a log file somewhere, or
+   print in the response buffer.
+*)
+
+let safe_prerr_endline s =
+  try prerr_endline s;flush stderr with _ -> ()
+
 let prerr_endline s =
-  if !debug then (prerr_endline s;flush stderr)
-let prerr_string s =
-  if !debug then (prerr_string s;flush stderr)
+  if !debug then try prerr_endline s;flush stderr with _ -> ()
 
 let lib_ide_file f =
   Filename.concat (Filename.concat !Minilib.coqlib "ide") f
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index f15cd120c3..fe8936877d 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -30,8 +30,12 @@ val is_char_start : char -> bool
 val lib_ide_file : string -> string
 val my_stat : string -> Unix.stats option
 
+(** safe version of Pervasives.prerr_endline
+    (avoid exception in win32 without console) *)
+val safe_prerr_endline : string -> unit
+(** debug printing *)
 val prerr_endline : string -> unit
-val prerr_string : string -> unit
+
 val print_id : 'a -> unit
 
 val revert_timer : GMain.Timeout.id option ref