Separated notice vs info messages, and cleaned up the interface a bit.

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

2 files changed, 23 insertions, 15 deletions

diff --git a/lib/pp.ml4 b/lib/pp.ml4
index f64f932e24..8974b89601 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -283,7 +283,8 @@ let emacs_quote strm =
     [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >]
   else hov 0 strm
 
-let warnbody strm = emacs_quote (str "Warning: " ++ strm)
+let warnbody strm = emacs_quote (str "Warning:" ++ spc () ++ strm)
+let errorbody strm = emacs_quote (str "Error:" ++ spc () ++ strm)
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
@@ -292,16 +293,6 @@ let pp_with ft strm =
 let ppnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
 
-let default_warn_with ft strm = ppnl_with ft (warnbody strm)
-
-let pp_warn_with = ref default_warn_with
-
-let set_warning_function pp_warn = pp_warn_with := pp_warn
-
-let warn_with ft strm = !pp_warn_with ft strm
-
-let warning_with ft string = warn_with ft (str string)
-
 let pp_flush_with ft = Format.pp_print_flush ft
 
 (* pretty printing functions WITH FLUSH *)
@@ -314,13 +305,15 @@ let msgnl_with ft strm =
 let msg_warning_with ft strm =
   msgnl_with ft (warnbody strm)
 
+let msg_error_with ft strm =
+  msgnl_with ft (errorbody strm)
+
 (* pretty printing functions WITHOUT FLUSH *)
 let pp        x = pp_with   !std_ft x
 let ppnl      x = ppnl_with !std_ft x
 let pperr     x = pp_with   !err_ft x
 let pperrnl   x = ppnl_with !err_ft x
 let message   s = ppnl      (str s)
-let warning   x = warning_with !err_ft x
 let pp_flush  x = Format.pp_print_flush !std_ft x
 let pperr_flush x = Format.pp_print_flush !err_ft x
 let flush_all () =
@@ -330,10 +323,12 @@ let flush_all () =
 let msg x = msg_with !std_ft x
 let msgnl x = msgnl_with !std_ft x
 let msg_info x = msgnl x
+let msg_notice x = msgnl x
 let msg_tactic x = msgnl x
 let msgerr x = msg_with !err_ft x
 let msgerrnl x = msgnl_with !err_ft x
 let msg_warning x = msg_warning_with !err_ft x
+let msg_error x = msg_error_with !err_ft x
 
 (* Same specific display in emacs as warning, but without the "Warning:" *)
 let msg_debug x = msgnl (emacs_quote x)
diff --git a/lib/pp.mli b/lib/pp.mli
index 6dcbc0411c..a0bc000ba8 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -77,9 +77,24 @@ val tclose : unit -> std_ppcmds
 (** {6 Sending messages to the user } *)
 
 val msg_info : std_ppcmds -> unit
+(** Message that displays information, usually in verbose mode, such as [Foobar
+    is defined] *)
+
+val msg_notice : std_ppcmds -> unit
+(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
+
 val msg_warning : std_ppcmds -> unit
-(* val msg_tactic : std_ppcmds -> unit *)
+(** Message indicating that something went wrong, but without serious 
+    consequences. *)
+
+val msg_error : std_ppcmds -> unit
+(** Message indicating that something went really wrong, though still 
+    recoverable; otherwise an exception would have been raised. *)
+
 val msg_debug : std_ppcmds -> unit
+(** For debugging purposes *)
+
+(** {6 Utilities} *)
 
 val string_of_ppcmds : std_ppcmds -> string
 
@@ -153,8 +168,6 @@ val pperr_flush : unit -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
-
 (** {6 Low-level pretty-printing functions {% \emph{%}with flush{% }%}. } *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit