4 files changed, 64 insertions, 16 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 5b66f9364..a48d05955 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -62,6 +62,11 @@ let verbosely f x = without_option silent f x
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
+(* Use terminal color *)
+let term_color = ref true
+let make_term_color b = term_color := b
+let is_term_color () = !term_color
+
 let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
diff --git a/lib/flags.mli b/lib/flags.mli
index c47996621..77399b9e5 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -47,6 +47,10 @@ val if_verbose : ('a -> unit) -> 'a -> unit
 val make_auto_intros : bool -> unit
 val is_auto_intros : unit -> bool
 
+(** Terminal colouring *)
+val make_term_color : bool -> unit
+val is_term_color : unit -> bool
+
 (** [program_cmd] indicates that the current command is a Program one.
     [program_mode] tells that Program mode has been activated, either
     globally via [Set Program] or locally via the Program command prefix. *)
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 8974b8960..0b207c7c3 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -283,8 +283,6 @@ 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:" ++ spc () ++ strm)
-let errorbody strm = emacs_quote (str "Error:" ++ spc () ++ strm)
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
@@ -302,12 +300,6 @@ let msg_with ft strm =
 let msgnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
 
-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
@@ -322,16 +314,50 @@ let flush_all () =
 (* pretty printing functions WITH FLUSH *)
 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)
+(* Logging management *)
+
+type level =
+| Debug of string
+| Info
+| Notice
+| Warning
+| Error
+
+type logger = level -> std_ppcmds -> unit
+
+let print_color s x =
+  if Flags.is_term_color () then
+    (str ("\027[" ^ s ^ "m")) ++ x ++ (str "\027[0m")
+  else x
+
+let make_body color info s =
+  emacs_quote (print_color color (print_color "1" (info ++ spc () ++ s)))
+
+let debugbody strm = print_color "36" (str "Debug:" ++ spc () ++ strm) (* cyan *)
+let warnbody strm = make_body "93" (str "Warning:") strm (* bright yellow *)
+let errorbody strm = make_body "31" (str "Error:") strm (* bright red *)
+
+let std_logger level msg = match level with
+| Debug _ -> msgnl (debugbody msg) (* cyan *)
+| Info -> msgnl (print_color "37" msg) (* gray *)
+| Notice -> msgnl msg
+| Warning -> msgnl_with !err_ft (warnbody msg) (* bright yellow *)
+| Error -> msgnl_with !err_ft (errorbody msg) (* bright red *)
+
+let logger = ref std_logger
+
+let msg_info x = !logger Info x
+let msg_notice x = !logger Notice x
+let msg_warning x = !logger Warning x
+let msg_error x = !logger Error x
+let msg_debug x = !logger (Debug "_") x
+
+let set_logger l = logger := l
+
+(** Utility *)
 
 let string_of_ppcmds c =
   msg_with Format.str_formatter c;
diff --git a/lib/pp.mli b/lib/pp.mli
index a0bc000ba..bc7d58a0b 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -76,6 +76,15 @@ val tclose : unit -> std_ppcmds
 
 (** {6 Sending messages to the user } *)
 
+type level =
+| Debug of string
+| Info
+| Notice
+| Warning
+| Error
+
+type logger = level -> std_ppcmds -> unit
+
 val msg_info : std_ppcmds -> unit
 (** Message that displays information, usually in verbose mode, such as [Foobar
     is defined] *)
@@ -94,6 +103,11 @@ val msg_error : std_ppcmds -> unit
 val msg_debug : std_ppcmds -> unit
 (** For debugging purposes *)
 
+val std_logger : logger
+(** Standard logging function *)
+
+val set_logger : logger -> unit
+
 (** {6 Utilities} *)
 
 val string_of_ppcmds : std_ppcmds -> string
@@ -171,4 +185,3 @@ val flush_all: unit -> unit
 (** {6 Low-level pretty-printing functions {% \emph{%}with flush{% }%}. } *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
-