Reworking the -color flag of coqtop.

5 files changed, 17 insertions, 16 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 1000101a42..1bcbd25fed 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -458,7 +458,6 @@ 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;
   while not !quit do
     try
       let xml_query = Xml_parser.parse xml_ic in
diff --git a/lib/flags.ml b/lib/flags.ml
index 993ebaa705..f95c31d9b8 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -141,11 +141,6 @@ 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 false
-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 cfc3d5001e..757563926c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -79,10 +79,6 @@ 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
-
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 01eaccd2bb..4eb75e0de7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -43,13 +43,23 @@ let warning s = msg_warning (strbrk s)
 
 let toploop = ref None
 
+let color : [`ON | `AUTO | `OFF] ref = ref `AUTO
+let set_color = function
+| "on" -> color := `ON
+| "off" -> color := `OFF
+| "auto" -> color := `AUTO
+| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
+
 let toploop_init = ref begin fun x ->
   let () =
-    if
+    let has_color = match !color with
+    | `OFF -> false
+    | `ON -> true
+    | `AUTO ->
       Terminal.has_style Unix.stdout &&
-      Terminal.has_style Unix.stderr &&
-      not (!Flags.print_emacs)
-    then begin
+      Terminal.has_style Unix.stderr
+    in
+    if has_color then begin
       let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
       match colors with
       | None ->
@@ -210,7 +220,7 @@ let set_emacs () =
   Flags.print_emacs := true;
   Pp.make_pp_emacs ();
   Vernacentries.qed_display_script := false;
-  Flags.make_term_color false
+  color := `OFF
 
 (** GC tweaking *)
 
@@ -447,7 +457,7 @@ let parse_args arglist =
     |"-beautify" -> make_beautify true
     |"-boot" -> boot := true; no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
-    |"-color" -> Flags.make_term_color true
+    |"-color" -> set_color (next ())
     |"-config"|"--config" -> print_config := true
     |"-debug" -> set_debug ()
     |"-emacs" -> set_emacs ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index eeea7b7a60..e098f70a82 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -59,6 +59,7 @@ let print_usage_channel co command =
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -emacs                 tells Coq it is executed under Emacs\
+\n  -color (on|off|auto)   configure color output (only active through coqtop)\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\