[pp] Move terminal-specific tagging to the toplevel.

Previously, tags were associated to terminal styles, which doesn't make
sense on terminal-free pretty printing scenarios.

This commit moves tag interpretation to the toplevel terminal handling
module `Topfmt`.

13 files changed, 90 insertions, 187 deletions

diff --git a/ide/richpp.mli b/ide/richpp.mli
index 0fe4315b7..ea4b189ba 100644
--- a/ide/richpp.mli
+++ b/ide/richpp.mli
@@ -19,7 +19,7 @@ type 'annotation located = {
 (* XXX: The width parameter should be moved to a `formatter_property`
    record shared with Topfmt *)
 
-(** [rich_pp width get_annotations ppcmds] returns the interpretation
+(** [rich_pp width ppcmds] returns the interpretation
     of [ppcmds] as a semi-structured document
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 5a5f6afd3..c73ae9b90 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -28,7 +28,6 @@ Util
 Stateid
 Pp
 Feedback
-Ppstyle
 CUnix
 Envars
 Aux_file
diff --git a/lib/pp.ml b/lib/pp.ml
index 53c1fb4c3..7b21f9bbd 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -288,4 +288,3 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
-
diff --git a/lib/pp.mli b/lib/pp.mli
index ff4206534..2c45ce0a7 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -160,12 +160,11 @@ val surround : std_ppcmds -> std_ppcmds
 (** Surround with parenthesis. *)
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-
 val pr_loc : Loc.t -> std_ppcmds
 
 (** {6 Main renderers, to formatter and to string } *)
 
-(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
+(** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
 val pp_with          : Format.formatter -> std_ppcmds -> unit
 
 val string_of_ppcmds : std_ppcmds -> string
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
deleted file mode 100644
index 6969c3d5c..000000000
--- a/lib/ppstyle.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module String = CString
-
-type t = Pp.pp_tag
-
-let tags : Terminal.style option String.Map.t ref = ref String.Map.empty
-
-let to_format tag = String.concat "." tag
-let of_format tag = String.split  '.' tag
-
-let make ?style tag =
-  let name = to_format tag                          in
-  let () = assert (not (String.Map.mem name !tags)) in
-  let () = tags := String.Map.add name style !tags  in
-  name
-
-let get_style tag =
-  try String.Map.find tag !tags
-  with Not_found -> assert false
-
-let set_style tag st =
-  try tags := String.Map.update tag st !tags
-  with Not_found -> assert false
-
-let clear_styles () =
-  tags := String.Map.map (fun _ -> None) !tags
-
-let dump () = String.Map.bindings !tags
-
-let parse_config s =
-  let styles = Terminal.parse s in
-  let set accu (name, st) =
-    try String.Map.update name (Some st) accu with Not_found -> accu
-  in
-  tags := List.fold_left set !tags styles
-
-(** Default tag is to reset everything *)
-let default = Terminal.({
-  fg_color = Some `DEFAULT;
-  bg_color = Some `DEFAULT;
-  bold = Some false;
-  italic = Some false;
-  underline = Some false;
-  negative = Some false;
-})
-
-let empty = Terminal.make ()
-
-let error_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
-  make ~style ["message"; "error"]
-
-let warning_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in
-  make ~style ["message"; "warning"]
-
-let debug_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in
-  make ~style ["message"; "debug"]
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
deleted file mode 100644
index 2690d3910..000000000
--- a/lib/ppstyle.mli
+++ /dev/null
@@ -1,50 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Highlighting of printers. Used for pretty-printing terms that should be
-    displayed on a color-capable terminal. *)
-
-(** {5 Style tags} *)
-
-(** This API is provisional and will likely be refined. *)
-type t = Pp.pp_tag
-
-(** Style tags *)
-
-val make : ?style:Terminal.style -> string list -> t
-(** Create a new tag with the given name. Each name must be unique. The optional
-    style is taken as the default one. *)
-
-(** {5 Manipulating global styles} *)
-
-val get_style : t -> Terminal.style option
-(** Get the style associated to a tag from a format tag. *)
-
-val set_style : t -> Terminal.style option -> unit
-(** Set a style associated to a tag. *)
-
-val clear_styles : unit -> unit
-(** Clear all styles. *)
-
-val parse_config : string -> unit
-(** Add all styles from the given string as parsed by {!Terminal.parse}.
-    Unregistered tags are ignored. *)
-
-val dump : unit -> (t * Terminal.style option) list
-(** Recover the list of known tags together with their current style. *)
-
-(** {5 Tags} *)
-
-val error_tag : t
-(** Tag used by the {!Pp.msg_error} function. *)
-
-val warning_tag : t
-(** Tag used by the {!Pp.msg_warning} function. *)
-
-val debug_tag : t
-(** Tag used by the {!Pp.msg_debug} function. *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d9410a088..dc418d530 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -29,17 +29,10 @@ open Printer
 
 module Tag =
 struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["tactic"; "keyword"]
 
-  let primitive =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["tactic"; "primitive"]
-
-  let string =
-    let style = Terminal.make ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["tactic"; "string"]
+  let keyword   = "tactic.keyword"
+  let primitive = "tactic.primitive"
+  let string    = "tactic.string"
 
 end
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c772f7be1..d92d83275 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -23,32 +23,14 @@ open Misctypes
 
 module Tag =
 struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["constr"; "keyword"]
+  let keyword   = "constr.keyword"
+  let evar      = "constr.evar"
+  let univ      = "constr.type"
+  let notation  = "constr.notation"
+  let variable  = "constr.variable"
+  let reference = "constr.reference"
+  let path      = "constr.path"
 
-  let evar =
-    let style = Terminal.make ~fg_color:`LIGHT_BLUE () in
-    Ppstyle.make ~style ["constr"; "evar"]
-
-  let univ =
-    let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in
-    Ppstyle.make ~style ["constr"; "type"]
-
-  let notation =
-    let style = Terminal.make ~fg_color:`WHITE () in
-    Ppstyle.make ~style ["constr"; "notation"]
-
-  let variable =
-    Ppstyle.make ["constr"; "variable"]
-
-  let reference =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["constr"; "reference"]
-
-  let path =
-    let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in
-    Ppstyle.make ~style ["constr"; "path"]
 end
 
 let do_not_tag _ x = x
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 521b4ec2a..baa1b8d79 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -28,12 +28,10 @@ open Goptions
 
 module Tag =
 struct
-  let definition =
-    let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["module"; "definition"]
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["module"; "keyword"]
+
+  let definition = "module.definition"
+  let keyword    = "module.keyword"
+
 end
 
 let tag t s = Pp.tag t s
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 43807c1ca..0cc6ca317 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -252,7 +252,7 @@ let print_toplevel_error (e, info) =
       else mt ()
     else print_location_in_file loc
   in
-  let hdr msg = hov 0 (tag Ppstyle.error_tag (str "Error:") ++ spc () ++ msg) in
+  let hdr msg = hov 0 (Topfmt.err_hdr ++ msg) in
   locmsg ++ hdr (CErrors.iprint (e, info))
 
 (* Read the input stream until a dot is encountered *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 268d40c91..c4d8dfec9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -67,8 +67,8 @@ let init_color () =
       ()
     | Some s ->
       (** Overwrite all colors *)
-      Ppstyle.clear_styles ();
-      Ppstyle.parse_config s;
+      Topfmt.clear_styles ();
+      Topfmt.parse_color_config s;
       Topfmt.init_color_output ()
   end
 
@@ -308,19 +308,16 @@ let usage () =
 
 let print_style_tags () =
   let () = init_color () in
-  let tags = Ppstyle.dump () in
+  let tags = Topfmt.dump_tags () in
   let iter (t, st) =
-    let st = match st with Some st -> st | None -> Terminal.make () in
-    let opt = Terminal.eval st ^ t ^   Terminal.reset ^ "\n" in
+    let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
     print_string opt
   in
-  let make (t, st) = match st with
-  | None -> None
-  | Some st ->
+  let make (t, st) =
     let tags = List.map string_of_int (Terminal.repr st) in
-    Some (t ^ "=" ^ String.concat ";" tags)
+    (t ^ "=" ^ String.concat ";" tags)
   in
-  let repr = List.map_filter make tags in
+  let repr = List.map make tags in
   let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in
   let () = List.iter iter tags in
   flush_all ()
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e5063e27b..f843484f7 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -97,6 +97,15 @@ let set_margin v =
 
 (** Console display of feedback *)
 
+(** Default tags *)
+module Tag = struct
+
+  let error   = "message.error"
+  let warning = "message.warning"
+  let debug   = "message.debug"
+
+end
+
 type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
 let msgnl_with fmt strm =
@@ -123,10 +132,10 @@ end
 
 open Emacs
 
-let  dbg_str = tag Ppstyle.debug_tag   (str "Debug:")   ++ spc ()
-let info_str = mt ()
-let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc ()
-let  err_str = tag Ppstyle.error_tag   (str "Error:")   ++ spc ()
+let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
+let info_hdr = mt ()
+let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
+let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
 
 let make_body quoter info ?loc s =
   let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
@@ -134,13 +143,13 @@ let make_body quoter info ?loc s =
 
 (* Generic logger *)
 let gen_logger dbg err ?loc level msg = match level with
-  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_str ?loc msg)
-  | Info    -> msgnl_with !std_ft (make_body dbg info_str ?loc msg)
+  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?loc msg)
+  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg)
   (* XXX: What to do with loc here? *)
   | Notice  -> msgnl_with !std_ft msg
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
+               msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?loc msg)
 
 (** Standard loggers *)
 
@@ -153,7 +162,43 @@ let std_logger ?loc level msg =
   gen_logger (fun x -> x) (fun x -> x) ?loc level msg;
   !std_logger_cleanup ()
 
-(** Color logging. Moved from pp_style, it may need some more refactoring  *)
+(** Color logging. Moved from Ppstyle, it may need some more refactoring  *)
+
+(* Tag map for terminal style *)
+let default_tag_map () = let open Terminal in [
+  (* Local to console toplevel *)
+    "message.error"    , make ~bold:true ~fg_color:`WHITE ~bg_color:`RED ()
+  ; "message.warning"  , make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW ()
+  ; "message.debug"    , make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA ()
+  (* Coming from the printer *)
+  ; "constr.evar"      , make            ~fg_color:`LIGHT_BLUE ()
+  ; "constr.keyword"   , make ~bold:true ()
+  ; "constr.type"      , make ~bold:true ~fg_color:`YELLOW ()
+  ; "constr.notation"  , make ~fg_color:`WHITE ()
+  (* ["constr"; "variable"] is not assigned *)
+  ; "constr.reference" , make ~fg_color:`LIGHT_GREEN ()
+  ; "constr.path"      , make ~fg_color:`LIGHT_MAGENTA ()
+  ; "module.definition", make ~bold:true ~fg_color:`LIGHT_RED ()
+  ; "module.keyword"   , make ~bold:true ()
+  ; "tactic.keyword"   , make ~bold:true ()
+  ; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
+  ; "tactic.string"    , make ~fg_color:`LIGHT_RED ()
+  ]
+
+let tag_map = ref CString.Map.empty
+
+let init_tag_map styles =
+  let set accu (name, st) = CString.Map.add name st accu in
+  tag_map := List.fold_left set !tag_map styles
+
+let clear_styles () =
+  tag_map := CString.Map.empty
+
+let parse_color_config file =
+  let styles = Terminal.parse file in
+  init_tag_map styles
+
+let dump_tags () = CString.Map.bindings !tag_map
 
 (** Not thread-safe. We should put a lock somewhere if we print from
     different threads. Do we? *)
@@ -175,9 +220,9 @@ let make_style_stack () =
   | st :: _ -> st
   in
   let push tag =
-    let style = match Ppstyle.get_style tag with
-      | None    -> empty
-      | Some st -> st
+    let style =
+      try CString.Map.find tag !tag_map
+      with | Not_found -> empty
     in
     (** Use the merging of the latest tag and the one being currently pushed.
     This may be useful if for instance the latest tag changes the background and
@@ -196,6 +241,7 @@ let make_style_stack () =
   push, pop, clear
 
 let init_color_output () =
+  init_tag_map (default_tag_map ());
   let push_tag, pop_tag, clear_tag = make_style_stack () in
   std_logger_cleanup := clear_tag;
   let tag_handler = {
@@ -220,8 +266,8 @@ let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
 let ft_logger old_logger ft ?loc level mesg =
   let id x = x in
   match level with
-  | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
-  | Info    -> msgnl_with ft (make_body id info_str mesg)
+  | Debug   -> msgnl_with ft (make_body id  dbg_hdr mesg)
+  | Info    -> msgnl_with ft (make_body id info_hdr mesg)
   | Notice  -> msgnl_with ft mesg
   | Warning -> old_logger ?loc level mesg
   | Error   -> old_logger ?loc level mesg
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 38a400cfd..1555f80a9 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -36,12 +36,18 @@ val get_depth_boxes : unit -> int option
 val set_margin : int option -> unit
 val get_margin : unit -> int option
 
+(** Headers for tagging *)
+val err_hdr : Pp.std_ppcmds
+
 (** Console display of feedback *)
 val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
 
 val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
 
 val init_color_output : unit -> unit
+val clear_styles : unit -> unit
+val parse_color_config : string -> unit
+val dump_tags : unit -> (string * Terminal.style) list
 
 (** [with_output_to_file file f x] executes [f x] with logging
     redirected to a file [file] *)