safe_prerr_endline in Minilib

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

8 files changed, 38 insertions, 36 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 6e8190722..dbb0d8ac3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -73,11 +73,11 @@ let check_connection args =
     | _ -> raise (Coqtop_output lines)
   with
     | End_of_file ->
-      safe_prerr_endline "Cannot start connection with coqtop";
+      Minilib.safe_prerr_endline "Cannot start connection with coqtop";
       exit 1
     | Coqtop_output lines ->
-      safe_prerr_endline "Connection with coqtop failed:";
-      List.iter safe_prerr_endline lines;
+      Minilib.safe_prerr_endline "Connection with coqtop failed:";
+      List.iter Minilib.safe_prerr_endline lines;
       exit 1
 
 (** It is tempting to merge the following function with the previous one,
@@ -98,11 +98,11 @@ let check_coqlib args =
     | _ -> raise (Coqtop_output lines)
   with
     | End_of_file ->
-      safe_prerr_endline "Cannot start connection with coqtop";
+      Minilib.safe_prerr_endline "Cannot start connection with coqtop";
       exit 1
     | Coqtop_output lines ->
-      safe_prerr_endline "Connection with coqtop failed:";
-      List.iter safe_prerr_endline lines;
+      Minilib.safe_prerr_endline "Connection with coqtop failed:";
+      List.iter Minilib.safe_prerr_endline lines;
       exit 1
 
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 85b331c43..900bd26bf 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -189,7 +189,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);*)
-  safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
+  Minilib.safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
   let count = ref 0 in
   List.iter
     (function {script=view; analyzed_view = av } ->
@@ -201,12 +201,12 @@ let crash_save i =
        in
        try
 	 if try_export filename (view#buffer#get_text ()) then
-	   safe_prerr_endline ("Saved "^filename)
-	 else safe_prerr_endline ("Could not save "^filename)
-       with _ -> safe_prerr_endline ("Could not save "^filename))
+	   Minilib.safe_prerr_endline ("Saved "^filename)
+	 else Minilib.safe_prerr_endline ("Could not save "^filename)
+       with _ -> Minilib.safe_prerr_endline ("Could not save "^filename))
     )
     session_notebook#pages;
-  safe_prerr_endline "Done. Please report.";
+  Minilib.safe_prerr_endline "Done. Please report.";
   if i <> 127 then exit i
 
 let ignore_break () =
@@ -1687,6 +1687,7 @@ let load_file handler f =
   try
     prerr_endline "Loading file starts";
     let is_f = Minilib.same_file f in
+      Minilib.safe_prerr_endline f;
       if not (Minilib.list_fold_left_i
 		(fun i found x -> if found then found else
                    let {analyzed_view=av} = x in
@@ -2931,10 +2932,10 @@ let process_argv argv =
   try
     let continue,filtered = Coq.filter_coq_opts (List.tl argv) in
     if not continue then
-      (List.iter safe_prerr_endline filtered; exit 0);
+      (List.iter Minilib.safe_prerr_endline filtered; exit 0);
     let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
     if opts <> [] then
-      (safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1);
+      (Minilib.safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1);
     filtered
   with _ ->
-    (safe_prerr_endline "coqtop choked on one of your option"; exit 1)
+    (Minilib.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 a9aed9599..f09ef2492 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -98,7 +98,7 @@ let () =
       with
 	| Sys.Break -> Ideutils.prerr_endline "Interrupted."
 	| e ->
-	    Ideutils.safe_prerr_endline
+	    Minilib.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 a8527ac01..c6994a8d9 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -31,15 +31,6 @@ 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 try prerr_endline s;flush stderr with _ -> ()
 
@@ -324,11 +315,11 @@ let url_for_keyword =
 	let u = String.sub s (i + 1) (String.length s - i - 1) in
 	Hashtbl.add ht k u
       with _ ->
-	safe_prerr_endline "Warning: Cannot parse documentation index file."
+	Minilib.safe_prerr_endline "Warning: Cannot parse documentation index file."
     done with End_of_file ->
       close_in cin
   with _ ->
-    safe_prerr_endline "Warning: Cannot find documentation index file."
+    Minilib.safe_prerr_endline "Warning: Cannot find documentation index file."
   end;
   Hashtbl.find ht : string -> string)
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 23b31e4ae..977aa0c14 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -30,9 +30,6 @@ 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
 
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 2182c45e0..96d257df6 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -75,6 +75,15 @@ let home =
 let coqlib = ref ""
 let coqtop_path = ref ""
 
+(* 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 _ -> ()
+
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p =
   let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 9c8cf0978..86f7c8a3f 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -26,6 +26,10 @@ val home : string
 val coqlib : string ref
 val coqtop_path : string ref
 
+(** safe version of Pervasives.prerr_endline
+    (avoid exception in win32 without console) *)
+val safe_prerr_endline : string -> unit
+
 val strip_path : string -> string
 val canonical_path_name : string -> string
 
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 95a0831d8..9c7a29045 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -47,10 +47,10 @@ let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = funct
   | ("-full"|"-opt") :: r ->
     process_cmd_line (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
-    prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n";
+    Minilib.safe_prerr_endline "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
     process_cmd_line opts (Arg "-impredicative_set" :: l) r
   | "-no-install" :: r ->
-    if not install then prerr_string "Warning: -no-install sets more than once.\n";
+    if not install then Minilib.safe_prerr_endline "Warning: -no-install sets more than once.";
     process_cmd_line (project_file,makefile,false,opt) l r
   | "-custom" :: com :: dependencies :: file :: r ->
     process_cmd_line opts (Special (file,dependencies,com) :: l) r
@@ -63,8 +63,8 @@ let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = funct
   | "-f" :: file :: r ->
     let () = match project_file with
       | None -> ()
-      | Some _ -> prerr_string
-	"Warning: Several features will not work with multiple project files.\n"
+      | Some _ -> Minilib.safe_prerr_endline
+	"Warning: Several features will not work with multiple project files."
     in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r)
   | ["-f"] ->
     raise Parsing_error
@@ -72,8 +72,7 @@ let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = funct
     let () = match makefile with
       |None -> ()
       |Some f ->
-	prerr_string "Warning: Only one output file in genererated. ";
-	prerr_string f; prerr_string " will not.\n"
+	Minilib.safe_prerr_endline ("Warning: Only one output file in genererated. "^f^" will not.")
     in process_cmd_line (project_file,Some file,install,opt) l r
   | v :: "=" :: def :: r ->
     process_cmd_line opts (Def (v,def) :: l) r
@@ -125,7 +124,8 @@ let read_project_file f = split_arguments (snd (process_cmd_line (Some f, None,
 let args_from_project file project_files =
   let contains_file f dir =
     let is_f = Minilib.same_file f in
-      List.exists (fun x -> is_f (if Filename.is_relative x then Filename.concat dir x else x))
+      List.exists (fun x -> let tmp = (if Filename.is_relative x then Filename.concat dir x else x)
+		   in Minilib.safe_prerr_endline tmp; is_f tmp)
   in try
       let (_,(_,(i_inc,r_inc),(args,_))) = List.find (fun (dir,((v_files,_,_,_),_,_)) ->
 							contains_file file dir v_files) project_files in