Cleaned prerr_endline use.

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

15 files changed, 127 insertions, 116 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index fae5cb7fc..dd0959726 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -293,11 +293,11 @@ let is_closed coqtop = coqtop.is_closed
 (** These are asynchronous signals *)
 let break_coqtop coqtop =
   try !interrupter coqtop.handle.pid
-  with _ -> prerr_endline "Error while sending Ctrl-C"
+  with _ -> Minilib.log "Error while sending Ctrl-C"
 
 let kill_coqtop coqtop =
   try !killer coqtop.handle.pid
-  with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
+  with _ -> Minilib.log "Kill -9 failed. Process already terminated ?"
 
 let unsafe_process coqtop f =
   coqtop.is_computing <- true;
@@ -363,7 +363,7 @@ let eval_call coqtop (c:'a Serialize.call) =
     let msg = Printf.sprintf "Error communicating with pid [%i]: %s"
       coqtop.pid (Printexc.to_string err)
     in
-    prerr_endline msg;
+    Minilib.log msg;
     raise DeadCoqtop
 
 let interp coqtop ?(raw=false) ?(verbose=true) s =
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6e3c85d47..dd2c95131 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -157,7 +157,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);*)
-  Minilib.safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
+  Minilib.log "Trying to save all buffers in .crashcoqide files";
   let count = ref 0 in
   List.iter
     (function {script=view; analyzed_view = av } ->
@@ -169,19 +169,19 @@ let crash_save i =
        in
        try
 	 if try_export filename (view#buffer#get_text ()) then
-	   Minilib.safe_prerr_endline ("Saved "^filename)
-	 else Minilib.safe_prerr_endline ("Could not save "^filename)
-       with _ -> Minilib.safe_prerr_endline ("Could not save "^filename))
+	   Minilib.log ("Saved "^filename)
+	 else Minilib.log ("Could not save "^filename)
+       with _ -> Minilib.log ("Could not save "^filename))
     )
     session_notebook#pages;
-  Minilib.safe_prerr_endline "Done. Please report.";
+  Minilib.log "Done. Please report.";
   if i <> 127 then exit i
 
 let ignore_break () =
   List.iter
     (fun i ->
       try Sys.set_signal i (Sys.Signal_handle crash_save)
-      with _ -> prerr_endline "Signal ignored (normal if Win32)")
+      with _ -> Minilib.log "Signal ignored (normal if Win32)")
     signals_to_crash;
   Sys.set_signal Sys.sigint Sys.Signal_ignore
 
@@ -189,24 +189,24 @@ let ignore_break () =
 exception Unsuccessful
 
 let force_reset_initial () =
-  prerr_endline "Reset Initial";
+  Minilib.log "Reset Initial";
   let term = session_notebook#current_term in
   Coq.reset_coqtop term.toplvl term.analyzed_view#requested_reset_initial
 
 let break () =
-  prerr_endline "User break received";
+  Minilib.log "User break received";
   Coq.break_coqtop session_notebook#current_term.toplvl
 
 let do_if_not_computing term text f =
   let threaded_task () =
-    let info () = prerr_endline ("Discarded query:" ^ text) in
+    let info () = Minilib.log ("Discarded query:" ^ text) in
     try Coq.try_grab term.toplvl f info
     with
     | e ->
       let msg = "Unknown error, please report:\n" ^ (Printexc.to_string e) in
       term.analyzed_view#set_message msg
   in
-  prerr_endline ("Launching thread " ^ text);
+  Minilib.log ("Launching thread " ^ text);
   ignore (Thread.create threaded_task ())
 
 let warning msg =
@@ -284,7 +284,7 @@ let setopts ct opts v =
 let get_current_word () =
   match session_notebook#current_term,cb#text with
     | {script=script; analyzed_view=av;},None ->
-      prerr_endline "None selected";
+      Minilib.log "None selected";
       let it = av#get_insert in
       let start = find_word_start it in
       let stop = find_word_end start in
@@ -292,8 +292,8 @@ let get_current_word () =
       script#buffer#move_mark `INSERT ~where:stop;
       script#buffer#get_text ~slice:true ~start ~stop ()
     | _,Some t ->
-      prerr_endline "Some selected";
-      prerr_endline t;
+      Minilib.log "Some selected";
+      Minilib.log t;
       t
 
 let input_channel b ic =
@@ -508,7 +508,7 @@ object(self)
             | 2 -> if self#save f then flash_info "Overwritten" else
                 flash_info "Could not overwrite file"
             | _ ->
-              prerr_endline "Auto revert set to false";
+              Minilib.log "Auto revert set to false";
               current.global_auto_revert <- false;
               disconnect_revert_timer ()
         else do_revert ()
@@ -548,7 +548,7 @@ object(self)
         | Some fn ->
           try
             last_auto_save_time <- Unix.time();
-            prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
+            Minilib.log ("Autosave time : "^(string_of_float (Unix.time())));
             if try_export fn (input_buffer#get_text ()) then begin
               flash_info ~delay:1000 "Autosaved"
             end
@@ -657,7 +657,7 @@ object(self)
             end
         end
       with
-        | e -> prerr_endline (Printexc.to_string e)
+        | e -> Minilib.log (Printexc.to_string e)
     end
 
   method private send_to_coq handle verbose phrase show_output show_error localize =
@@ -686,7 +686,7 @@ object(self)
         end
       end in
       full_goal_done <- false;
-      prerr_endline "Send_to_coq starting now";
+      Minilib.log "Send_to_coq starting now";
       (* It's important here to work with [ct] and not [!mycoqtop], otherwise
          we could miss a restart of coqtop and continue sending it orders. *)
       match Coq.interp handle ~verbose phrase with
@@ -697,7 +697,7 @@ object(self)
 
   (* This method is intended to perform stateless commands *)
   method raw_coq_query handle phrase =
-    let () = prerr_endline "raw_coq_query starting now" in
+    let () = Minilib.log "raw_coq_query starting now" in
     let display_error s =
       if not (Glib.Utf8.validate s) then
         flash_info "This error is so nasty that I can't even display it."
@@ -724,7 +724,7 @@ object(self)
     with Not_found -> None
 
 (*  method private process_phrase verbosely =
-    prerr_endline "process_phrase starting now";
+    Minilib.log "process_phrase starting now";
     let get_next_phrase () =
       self#find_phrase_starting_at self#get_start_of_input
     in
@@ -754,7 +754,7 @@ object(self)
   method private process_one_phrase handle verbosely do_highlight =
     let get_next_phrase () =
       self#clear_message;
-      prerr_endline "process_one_phrase starting now";
+      Minilib.log "process_one_phrase starting now";
       if do_highlight then begin
         push_info "Coq is computing";
         input_view#set_editable false;
@@ -767,12 +767,12 @@ object(self)
           end;
           None
         | Some(start,stop) ->
-          prerr_endline "process_one_phrase : to_process highlight";
+          Minilib.log "process_one_phrase : to_process highlight";
           if do_highlight then begin
             input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
-            prerr_endline "process_one_phrase : to_process applied";
+            Minilib.log "process_one_phrase : to_process applied";
           end;
-          prerr_endline "process_one_phrase : getting phrase";
+          Minilib.log "process_one_phrase : getting phrase";
           Some((start,stop),start#get_slice ~stop) in
     let remove_tag (start,stop) =
       if do_highlight then begin
@@ -965,7 +965,7 @@ object(self)
 
   (* backtrack Coq to the phrase preceding iterator [i] *)
   method private backtrack_to_no_lock handle i =
-    prerr_endline "Backtracking_to iter starts now.";
+    Minilib.log "Backtracking_to iter starts now.";
     full_goal_done <- false;
     (* pop Coq commands until we reach iterator [i] *)
     let rec n_step n =
@@ -997,7 +997,7 @@ object(self)
       (push_info "Undoing...";
        self#backtrack_to_no_lock handle i; Mutex.unlock coq_may_stop;
        pop_info ())
-    else prerr_endline "backtrack_to : discarded (lock is busy)"
+    else Minilib.log "backtrack_to : discarded (lock is busy)"
 
   method go_to_insert handle =
     let point = self#get_insert in
@@ -1024,7 +1024,7 @@ object(self)
        );
        pop_info ();
        Mutex.unlock coq_may_stop)
-    else prerr_endline "undo_last_step discarded"
+    else Minilib.log "undo_last_step discarded"
 
 
   method tactic_wizard handle l =
@@ -1097,7 +1097,7 @@ object(self)
                 if (it#compare self#get_start_of_input)<0
                 then GtkSignal.stop_emit ();
                 if String.length s > 1 then
-                  (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor ~where:it)));
+                  (Minilib.log "insert_text: Placing cursor";input_buffer#place_cursor ~where:it)));
     ignore (input_buffer#connect#after#apply_tag
               ~callback:(fun tag ~start ~stop ->
                 if (start#compare self#get_start_of_input)>=0
@@ -1148,14 +1148,14 @@ object(self)
                 match GtkText.Mark.get_name m  with
                   | Some "insert" -> ()
                   | Some s ->
-                    prerr_endline (s^" moved")
+                    Minilib.log (s^" moved")
                   | None -> () )
     );
     ignore (input_buffer#connect#insert_text
               ~callback:(fun it s ->
-                prerr_endline "Should recenter ?";
+                Minilib.log "Should recenter ?";
                 if String.contains s '\n' then begin
-                  prerr_endline "Should recenter : yes";
+                  Minilib.log "Should recenter : yes";
                   self#recenter_insert
                 end));
     let callback () =
@@ -1431,7 +1431,7 @@ let do_print session =
 let load_file handler f =
   let f = CUnix.correct_path f (Sys.getcwd ()) in
   try
-    prerr_endline "Loading file starts";
+    Minilib.log "Loading file starts";
     let is_f = CUnix.same_file f in
       if not (Util.list_fold_left_i
 		(fun i found x -> if found then found else
@@ -1444,31 +1444,31 @@ let load_file handler f =
 			    else false))
               0 false session_notebook#pages)
       then begin
-	prerr_endline "Loading: must open";
+	Minilib.log "Loading: must open";
 	let b = Buffer.create 1024 in
-	prerr_endline "Loading: get raw content";
+	Minilib.log "Loading: get raw content";
 	with_file handler f ~f:(input_channel b);
-	prerr_endline "Loading: convert content";
+	Minilib.log "Loading: convert content";
 	let s = do_convert (Buffer.contents b) in
-	prerr_endline "Loading: create view";
+	Minilib.log "Loading: create view";
 	let session = create_session (Some f) in
-	prerr_endline "Loading: adding view";
+	Minilib.log "Loading: adding view";
 	let index = session_notebook#append_term session in
 	let av = session.analyzed_view in
-	prerr_endline "Loading: stats";
+	Minilib.log "Loading: stats";
 	av#update_stats;
 	let input_buffer = session.script#buffer in
-	prerr_endline "Loading: fill buffer";
+	Minilib.log "Loading: fill buffer";
 	input_buffer#set_text s;
 	input_buffer#place_cursor ~where:input_buffer#start_iter;
 	force_retag input_buffer;
-	prerr_endline ("Loading: switch to view "^ string_of_int index);
+	Minilib.log ("Loading: switch to view "^ string_of_int index);
 	session_notebook#goto_page index;
-	prerr_endline "Loading: highlight";
+	Minilib.log "Loading: highlight";
 	input_buffer#set_modified false;
-	prerr_endline "Loading: clear undo";
+	Minilib.log "Loading: clear undo";
 	session.script#clear_undo ();
-	prerr_endline "Loading: success";
+	Minilib.log "Loading: success";
         !refresh_editor_hook ();
       end
   with
@@ -1742,7 +1742,7 @@ let main files =
           Format.fprintf fmt "@[match var with@\n%aend@]@."
             (print_list print_branch) cases;
           let s = Buffer.contents b in
-          prerr_endline s;
+          Minilib.log s;
           let {script = view } = session_notebook#current_term in
           ignore (view#buffer#delete_selection ());
           let m = view#buffer#create_mark
@@ -1953,7 +1953,7 @@ let main files =
              try GtkSignal.emit_unit
                    session_notebook#current_term.script#as_view
                    ~sgn:GtkText.View.S.paste_clipboard
-             with _ -> prerr_endline "EMIT PASTE FAILED") ~stock:`PASTE;
+             with _ -> Minilib.log "EMIT PASTE FAILED") ~stock:`PASTE;
       GAction.add_action "Find" ~stock:`FIND
         ~callback:(fun _ -> session_notebook#current_term.finder#show_find ());
       GAction.add_action "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3"
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 2dbb3f499..70c50e7ed 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -97,9 +97,9 @@ let () =
       try
 	GtkThread.main ()
       with
-	| Sys.Break -> Minilib.prerr_endline "Interrupted."
+	| Sys.Break -> Minilib.log "Interrupted."
 	| e ->
-	    Minilib.safe_prerr_endline
+	    Minilib.log
 	      ("CoqIde unexpected error:" ^ (Printexc.to_string e));
 	    Coqide.crash_save 127
     done
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 590a3493f..d5972ed1a 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -45,25 +45,25 @@ let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it
 
 let find_word_start (it:GText.iter) =
   let rec step_to_start it =
-    prerr_endline "Find word start";
+    Minilib.log "Find word start";
     if not it#nocopy#backward_char then
-      (prerr_endline "find_word_start: cannot backward"; it)
+      (Minilib.log "find_word_start: cannot backward"; it)
     else if is_word_char it#char
     then step_to_start it
     else (it#nocopy#forward_char;
-	prerr_endline ("Word start at: "^(string_of_int it#offset));it)
+	Minilib.log ("Word start at: "^(string_of_int it#offset));it)
   in
     step_to_start it#copy
 
 let find_word_end (it:GText.iter) =
   let rec step_to_end (it:GText.iter) =
-    prerr_endline "Find word end";
+    Minilib.log "Find word end";
     let c = it#char in
     if c<>0 && is_word_char c then (
       ignore (it#nocopy#forward_char);
       step_to_end it
     ) else (
-      prerr_endline ("Word end at: "^(string_of_int it#offset));
+      Minilib.log ("Word end at: "^(string_of_int it#offset));
       it)
   in
     step_to_end it#copy
@@ -76,11 +76,11 @@ let get_word_around (it:GText.iter) =
 
 
 let rec complete_backward w (it:GText.iter) =
-  prerr_endline "Complete backward...";
+  Minilib.log "Complete backward...";
   match it#backward_search w with
-    | None -> (prerr_endline "backward_search failed";None)
+    | None -> (Minilib.log "backward_search failed";None)
     | Some (start,stop) ->
-	prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
+	Minilib.log ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
 	if starts_word start then
 	  let ne = find_word_end stop in
 	    if ne#compare stop = 0
@@ -90,7 +90,7 @@ let rec complete_backward w (it:GText.iter) =
 
 
 let rec complete_forward w (it:GText.iter) =
-  prerr_endline "Complete forward...";
+  Minilib.log "Complete forward...";
   match it#forward_search w with
     | None -> None
     | Some (start,stop) ->
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 3f9bb3aca..ddf95e25e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -50,13 +50,13 @@ let byte_offset_to_char_offset s byte_offset =
   end
 
 let print_id id =
-  prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
+  Minilib.log ("GOT sig id :"^(string_of_int (Obj.magic id)))
 
 
 let do_convert s =
   Utf8_convert.f
     (if Glib.Utf8.validate s then begin
-      prerr_endline "Input is UTF-8";s
+      Minilib.log "Input is UTF-8";s
     end else
 	let from_loc () =
 	  let _,char_set = Glib.Convert.get_charset () in
@@ -88,26 +88,26 @@ let try_export file_name s =
   try let s =
     try match current.encoding with
       |Eutf8 -> begin
-	(prerr_endline "UTF-8 is enforced" ;s)
+	(Minilib.log "UTF-8 is enforced" ;s)
       end
       |Elocale -> begin
 	let is_unicode,char_set = Glib.Convert.get_charset () in
 	if is_unicode then
-	  (prerr_endline "Locale is UTF-8" ;s)
+	  (Minilib.log "Locale is UTF-8" ;s)
 	else
-	  (prerr_endline ("Locale is "^char_set);
+	  (Minilib.log ("Locale is "^char_set);
 	   Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
       end
       |Emanual enc ->
-	(prerr_endline ("Manual charset is "^ enc);
+	(Minilib.log ("Manual charset is "^ enc);
        Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:enc s)
-    with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
+    with e -> (Minilib.log ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
   in
   let oc = open_out file_name in
   output_string oc s;
   close_out oc;
   true
-  with e -> prerr_endline (Printexc.to_string e);false
+  with e -> Minilib.log (Printexc.to_string e);false
 
 let my_stat f = try Some (Unix.stat f) with _ -> None
 
@@ -227,16 +227,16 @@ let mutex text f =
     if Mutex.try_lock m
     then
       (try
-        prerr_endline ("Got lock on "^text);
+        Minilib.log ("Got lock on "^text);
         f x;
         Mutex.unlock m;
-        prerr_endline ("Released lock on "^text)
+        Minilib.log ("Released lock on "^text)
       with e ->
         Mutex.unlock m;
-        prerr_endline ("Released lock on "^text^" (on error)");
+        Minilib.log ("Released lock on "^text^" (on error)");
         raise e)
     else
-      prerr_endline
+      Minilib.log
         ("Discarded call for "^text^": computations ongoing")
 
 
@@ -314,11 +314,11 @@ let url_for_keyword =
 		let u = String.sub s (i + 1) (String.length s - i - 1) in
 		  Hashtbl.add ht k u
 	      with _ ->
-		Minilib.safe_prerr_endline "Warning: Cannot parse documentation index file."
+		Minilib.log "Warning: Cannot parse documentation index file."
 	  done with End_of_file ->
 	    close_in cin
       with _ ->
-	Minilib.safe_prerr_endline "Warning: Cannot find documentation index file."
+	Minilib.log "Warning: Cannot find documentation index file."
       end;
       Hashtbl.find ht : string -> string)
 
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 5638934bd..04bd4c454 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -6,13 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+type level = [
+  | `DEBUG
+  | `INFO
+  | `NOTICE
+  | `WARNING
+  | `ERROR
+  | `FATAL ]
+
 (** Some excerpt of Util and similar files to avoid loading the whole
     module and its dependencies (and hence Compat and Camlp4) *)
 
-let debug = ref (false)
-
-let prerr_endline s =
-  if !debug then try prerr_endline s;flush stderr with _ -> ()
+let debug = ref false
 
 (* On a Win32 application with no console, writing to stderr raise
    a Sys_error "bad file descriptor", hence the "try" below.
@@ -20,5 +25,5 @@ let prerr_endline s =
    print in the response buffer.
 *)
 
-let safe_prerr_endline s =
-  try prerr_endline s;flush stderr with _ -> ()
+let log ?(level = `DEBUG) msg =
+  if !debug then try prerr_endline msg; flush stderr with _ -> ()
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 1254f5a6d..c84321211 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -9,10 +9,16 @@
 (** Some excerpts of Util and similar files to avoid depending on them
     and hence on Compat and Camlp4 *)
 
+type level = [
+  | `DEBUG
+  | `INFO
+  | `NOTICE
+  | `WARNING
+  | `ERROR
+  | `FATAL ]
+
 (** debug printing *)
 val debug : bool ref
-val prerr_endline : string -> unit
 
-(** safe version of Pervasives.prerr_endline
-    (avoid exception in win32 without console) *)
-val safe_prerr_endline : string -> unit
+val log : ?level:level -> string -> unit
+
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 27245dd00..c8e7430f9 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -9,28 +9,28 @@
 open Configwin
 open Printf
 
-let pref_file = Filename.concat (Envars.xdg_config_home Minilib.prerr_endline) "coqiderc"
-let accel_file = Filename.concat (Envars.xdg_config_home Minilib.prerr_endline) "coqide.keys"
+let pref_file = Filename.concat (Envars.xdg_config_home Minilib.log) "coqiderc"
+let accel_file = Filename.concat (Envars.xdg_config_home Minilib.log) "coqide.keys"
 let lang_manager = GSourceView2.source_language_manager ~default:true
 let () = lang_manager#set_search_path
-  ((Envars.xdg_data_dirs Minilib.prerr_endline)@lang_manager#search_path)
+  ((Envars.xdg_data_dirs Minilib.log)@lang_manager#search_path)
 let style_manager = GSourceView2.source_style_scheme_manager ~default:true
 let () = style_manager#set_search_path
-  ((Envars.xdg_data_dirs Minilib.prerr_endline)@style_manager#search_path)
+  ((Envars.xdg_data_dirs Minilib.log)@style_manager#search_path)
 
 let get_config_file name =
   let find_config dir = Sys.file_exists (Filename.concat dir name) in
-  let config_dir = List.find find_config (Envars.xdg_config_dirs Minilib.prerr_endline) in
+  let config_dir = List.find find_config (Envars.xdg_config_dirs Minilib.log) in
   Filename.concat config_dir name
 
 (* Small hack to handle v8.3 to v8.4 change in configuration file *)
 let loaded_pref_file =
   try get_config_file "coqiderc"
-  with Not_found -> Filename.concat (Envars.home Minilib.prerr_endline) ".coqiderc"
+  with Not_found -> Filename.concat (Envars.home Minilib.log) ".coqiderc"
 
 let loaded_accel_file =
   try get_config_file "coqide.keys"
-  with Not_found -> Filename.concat (Envars.home Minilib.prerr_endline) ".coqide.keys"
+  with Not_found -> Filename.concat (Envars.home Minilib.log) ".coqide.keys"
 
 let mod_to_str (m:Gdk.Tags.modifier) =
   match m with
@@ -223,8 +223,8 @@ let current = {
   }
 
 let save_pref () =
-  if not (Sys.file_exists (Envars.xdg_config_home Minilib.prerr_endline))
-  then Unix.mkdir (Envars.xdg_config_home Minilib.prerr_endline) 0o700;
+  if not (Sys.file_exists (Envars.xdg_config_home Minilib.log))
+  then Unix.mkdir (Envars.xdg_config_home Minilib.log) 0o700;
   let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let p = current in
 
@@ -341,7 +341,7 @@ let load_pref () =
         v <> Coq_config.wwwcoq ^ "doc" &&
 	v <> Coq_config.wwwcoq ^ "doc/"
       then
-	(*prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*)
+	(* ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*)
       np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
     set_bool "show_toolbar" (fun v -> np.show_toolbar <- v);
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 0a2720c46..87ddee081 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -53,19 +53,19 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
   | ("-full"|"-opt") :: r ->
     process_cmd_line orig_dir (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
-    Minilib.safe_prerr_endline "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
+    Minilib.log "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
     process_cmd_line orig_dir opts (Arg "-impredicative_set" :: l) r
   | "-no-install" :: r ->
-    Minilib.safe_prerr_endline "Option -no-install is deprecated. Use \"-install none\" instead";
+    Minilib.log "Option -no-install is deprecated. Use \"-install none\" instead";
     process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
   | "-install" :: d :: r ->
-    if install <> UnspecInstall then Minilib.safe_prerr_endline "Warning: -install sets more than once.";
+    if install <> UnspecInstall then Minilib.log "Warning: -install sets more than once.";
     let install =
       match d with
 	| "user" -> UserInstall
 	| "none" -> NoInstall
 	| "global" -> TraditionalInstall
-	| _ -> Minilib.safe_prerr_endline (String.concat "" ["Warning: invalid option '"; d; "' passed to -install."]);
+	| _ -> Minilib.log (String.concat "" ["Warning: invalid option '"; d; "' passed to -install."]);
           install
     in
     process_cmd_line orig_dir (project_file,makefile,install,opt) l r
@@ -81,7 +81,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match project_file with
       | None -> ()
-      | Some _ -> Minilib.safe_prerr_endline
+      | Some _ -> Minilib.log
 	"Warning: Several features will not work with multiple project files."
     in
     let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
@@ -96,7 +96,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
 	let () = match makefile with
 	  |None -> ()
 	  |Some f ->
-	     Minilib.safe_prerr_endline ("Warning: Only one output file is genererated. "^f^" will not be.")
+	     Minilib.log ("Warning: Only one output file is genererated. "^f^" will not be.")
 	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
       end
   | v :: "=" :: def :: r ->
@@ -182,7 +182,7 @@ let args_from_project file project_files default_name =
 	  if contains_file dir v_files
 	  then build_cmd_line i_inc r_inc args
 	  else let newdir = Filename.dirname dir in
-	    Minilib.safe_prerr_endline newdir;
+	    Minilib.log newdir;
 	    if dir = newdir then [] else find_project_file newdir
       with Sys_error s ->
 	let newdir = Filename.dirname dir in
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 7dbd04529..4f8a3a10f 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -38,7 +38,7 @@ class type widget =
 let file_html_config = Filename.concat Configwin_messages.home ".configwin_html"
 
 let debug = false
-let dbg = if debug then prerr_endline else (fun _ -> ())
+let dbg s = if debug then Minilib.log s else ()
 
 (** Return the config group for the html config file,
    and the option for bindings. *)
diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml
index 6cd3ef579..dbb490033 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/utils/configwin_messages.ml
@@ -30,7 +30,7 @@ let version = "1.2";;
 
 let html_config = "Configwin bindings configurator for html parameters"
 
-let home = Envars.home ~warn:Minilib.prerr_endline
+let home = Envars.home ~warn:Minilib.log
 
 let mCapture = "Capture";;
 let mType_key = "Type key" ;;
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index 5e2b1e7c2..ace751c64 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -52,7 +52,7 @@ let string_to_key s =
       | '4' -> `MOD4
       | '5' -> `MOD5
       | _ ->
-	  prerr_endline s;
+	  Minilib.log s;
 	  raise Not_found
       in
       mask := m :: !mask
@@ -65,7 +65,7 @@ let string_to_key s =
     !mask, List.assoc key name_to_keysym
   with
     e ->
-      prerr_endline s;
+      Minilib.log s;
       raise e
 
 let key_to_string (m, k) =
@@ -116,7 +116,7 @@ let value_to_key v =
   match v with
     Raw.String s -> string_to_key s
   | _ ->
-      prerr_endline "value_to_key";
+      Minilib.log "value_to_key";
       raise Not_found
 
 let key_to_value k =
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 579392664..6b174ecbe 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -107,7 +107,7 @@ let key_press w ev =
 	  (fun h ->
 	    if h.cond () then
 	      try h.cback ()
-	      with e -> prerr_endline (Printexc.to_string e)
+	      with e -> Minilib.log (Printexc.to_string e)
 	    else ()
 	  )
 	  l;
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 9d1951851..a43fdc7c8 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -88,7 +88,7 @@ object(self)
     in
     let on_activate c () =
       if List.mem combo#entry#text Coq_commands.state_preserving then c ()
-      else prerr_endline "Not a state preserving command"
+      else Minilib.log "Not a state preserving command"
     in
     let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
     entry#misc#set_can_default true;
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 1e5dff349..2dae029ee 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -96,14 +96,14 @@ object (self)
       Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l
     in
     if false (* !debug *) then begin
-      prerr_endline "==========Undo Stack top=============";
+      Minilib.log "==========Undo Stack top=============";
       List.iter iter history;
       Printf.eprintf "Stack size %d\n" (List.length history);
-      prerr_endline "==========Undo Stack Bottom==========";
-      prerr_endline "==========Redo Stack start=============";
+      Minilib.log "==========Undo Stack Bottom==========";
+      Minilib.log "==========Redo Stack start=============";
       List.iter iter redo;
       Printf.eprintf "Stack size %d\n" (List.length redo);
-      prerr_endline "==========Redo Stack End=========="
+      Minilib.log "==========Redo Stack End=========="
     end
 
   method clear_undo () =
@@ -136,23 +136,23 @@ object (self)
 
   method undo () =
     if Mutex.try_lock undo_lock then begin
-      prerr_endline "UNDO";
+      Minilib.log "UNDO";
       let effective = self#process_action history in
       if effective then self#backward ();
       Mutex.unlock undo_lock;
       effective
     end else
-      (prerr_endline "UNDO DISCARDED"; true)
+      (Minilib.log "UNDO DISCARDED"; true)
 
   method redo () =
     if Mutex.try_lock undo_lock then begin
-      prerr_endline "REDO";
+      Minilib.log "REDO";
       let effective = self#process_action redo in
       if effective then self#forward ();
       Mutex.unlock undo_lock;
       effective
     end else
-      (prerr_endline "REDO DISCARDED"; true)
+      (Minilib.log "REDO DISCARDED"; true)
 
   method private handle_insert iter s =
     if Mutex.try_lock undo_lock then begin
@@ -177,12 +177,12 @@ object (self)
 
   method private do_auto_complete () =
     let iter = self#buffer#get_iter `INSERT in
-    prerr_endline ("Completion at offset: " ^ string_of_int iter#offset);
+    Minilib.log ("Completion at offset: " ^ string_of_int iter#offset);
     let start = find_word_start iter in
     if ends_word iter#backward_char then begin
       let w = self#buffer#get_text ~start ~stop:iter () in
       if String.length w >= auto_complete_length then begin
-        prerr_endline ("Completion of prefix: '" ^ w ^ "'");
+        Minilib.log ("Completion of prefix: '" ^ w ^ "'");
         let (off, prefix, proposals) = last_completion in
         let new_proposals = 
         (* check whether we have the last request in cache *)