Added a color output to Coqtop.

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

7 files changed, 74 insertions, 21 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
-
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3263de8d5..445908fba 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -136,13 +136,13 @@ END
 let test_plurial_form = function
   | [(_,([_],_))] ->
       Flags.if_verbose msg_warning
-   (str "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
+   (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
   | _ -> ()
 
 let test_plurial_form_types = function
   | [([_],_)] ->
       Flags.if_verbose msg_warning
-   (str "Keywords Implicit Types expect more than one type")
+   (strbrk "Keywords Implicit Types expect more than one type")
   | _ -> ()
 
 (* Gallina declarations *)
@@ -423,7 +423,7 @@ GEXTEND Gram
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
 	  Flags.if_verbose
-            msg_warning (str "Include Type is deprecated; use Include instead");
+            msg_warning (strbrk "Include Type is deprecated; use Include instead");
           VernacInclude(e::l) ] ]
   ;
   export_token:
@@ -629,7 +629,7 @@ GEXTEND Gram
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
 	   Flags.if_verbose
-             msg_warning (str "Arguments Scope is deprecated; use Arguments instead");
+             msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
 	 VernacArgumentsScope (use_section_locality (),qid,scl)
 
       (* Implicit *)
@@ -637,7 +637,7 @@ GEXTEND Gram
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   Flags.if_verbose
-             msg_warning (str "Implicit Arguments is deprecated; use Arguments instead");
+             msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 779cd06bf..6bbe6b026 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -256,9 +256,11 @@ let parse_args arglist =
     | "-emacs" :: rem ->
 	Flags.print_emacs := true; Pp.make_pp_emacs();
 	Vernacentries.qed_display_script := false;
+        Flags.make_term_color false;
 	parse rem
     | "-emacs-U" :: rem ->
 	warning "Obsolete option \"-emacs-U\", use -emacs instead.";	
+        Flags.make_term_color false;
 	parse ("-emacs" :: rem)
 
     | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
@@ -301,6 +303,8 @@ let parse_args arglist =
 
     | "-filteropts" :: rem -> filter_opts := true; parse rem
 
+    | "-nocolor" :: rem -> Flags.make_term_color false; parse rem
+
     | s :: rem ->
       if !filter_opts then
        s :: (parse rem)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4ba60d8e0..9d5d7d719 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -418,6 +418,7 @@ let loop () =
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
+  Flags.make_term_color false;
   try
     while true do
       let xml_answer =