From f0226504cfb179a4491d43764bfdb22a1fe2d106 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2011 20:53:35 +0000
Subject: A pass on warning printings. Made systematic the use of msg_warning
 so as to ensure the warning is flushed in real time. Made systematic the use
 of if_warn instead of if_verbose when the warning is intended to signal
 something anormal (if_warn is activated when compiling verbosely and when
 working interactively while if_verbose is activated only when working
 interactively and when loading verbosely).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/goptions.ml |  4 ++--
 library/library.ml  |  6 +++---
 library/nametab.ml  | 14 +++++++-------
 3 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'library')

diff --git a/library/goptions.ml b/library/goptions.ml
index d882ed944a..f5100a14a9 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -335,12 +335,12 @@ let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
   try set_option_value locality check_bool_value key v
-  with UserError (_,s) -> Flags.if_verbose msg_warning s
+  with UserError (_,s) -> Flags.if_warn msg_warning s
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
   try set_option_value locality check_unset_value key ()
-  with UserError (_,s) -> Flags.if_verbose msg_warning s
+  with UserError (_,s) -> Flags.if_warn msg_warning s
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
diff --git a/library/library.ml b/library/library.ml
index 071c7a46c6..3762287482 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -463,9 +463,9 @@ let rec_intern_by_filename_only id f =
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
-      Flags.if_verbose warning
-	((string_of_dirpath m.library_name)^" is already loaded from file "^
-	library_full_filename m.library_name);
+      Flags.if_warn msg_warning
+	(pr_dirpath m.library_name ++ str " is already loaded from file " ++
+	str (library_full_filename m.library_name));
       m.library_name, []
     end
  else
diff --git a/library/nametab.ml b/library/nametab.ml
index c6f04b0162..6dbd927d85 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -108,9 +108,9 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		  Flags.if_verbose
-		    warning ("Trying to mask the absolute name \""
-			     ^ U.to_string n ^ "\"!");
+		  Flags.if_warn
+		    msg_warning (str ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!"));
 		  current
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
@@ -131,7 +131,7 @@ struct
 		   become unaccessible forever *)
 		(* But ours is also absolute! This is an error! *)
 		error ("Cannot mask the absolute name \""
-  		       ^ U.to_string uname' ^ "\"!")
+		       ^ U.to_string uname' ^ "\"!")
 	  | Nothing
 	  | Relative _ -> Absolute (uname,o), dirmap
 
@@ -148,9 +148,9 @@ let rec push_exactly uname o level (current,dirmap) = function
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		  Flags.if_verbose
-		    warning ("Trying to mask the absolute name \""
-  			     ^ U.to_string n ^ "\"!");
+		  Flags.if_warn
+		    msg_warning (str ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!"));
 		  current
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
-- 
cgit v1.2.3