[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`

This is what has always been used, so it doesn't represent a functional
change.

This is just a preliminary patch, but many more possibilities could be
done wrt tags.

15 files changed, 67 insertions, 114 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index dbebe6a48..9cbc3fb6d 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -22,7 +22,7 @@ exception Anomaly of string option * std_ppcmds (* System errors *)
  * Anyways, tagging should not happen here, but in the specific
  * listener to the msg_* stuff.
  *)
-let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
+let tag_err_str s = tag Ppstyle.error_tag (str s) ++ spc ()
 let err_str       = tag_err_str "Error:"
 let ann_str       = tag_err_str "Anomaly:"
 
@@ -154,6 +154,6 @@ let handled e =
 
 let fatal_error info anomaly =
   let msg = info ++ fnl () in
-  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
+  pp_with !Pp_control.err_ft msg;
   Format.pp_print_flush !Pp_control.err_ft ();
   exit (if anomaly then 129 else 1)
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 57c6f30a4..e723bf4ba 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -73,10 +73,10 @@ end
 
 open Emacs
 
-let  dbg_str = tag Ppstyle.(Tag.inj debug_tag   tag) (str "Debug:")   ++ spc ()
+let  dbg_str = tag Ppstyle.debug_tag   (str "Debug:")   ++ spc ()
 let info_str = mt ()
-let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc ()
-let  err_str = tag Ppstyle.(Tag.inj error_tag   tag) (str "Error:"  ) ++ spc ()
+let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc ()
+let  err_str = tag Ppstyle.error_tag   (str "Error:"  ) ++ spc ()
 
 let make_body quoter info ?loc s =
   let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
@@ -132,7 +132,7 @@ let make_style_stack () =
   | st :: _ -> st
   in
   let push tag =
-    let style = match Ppstyle.get_style tag with
+    let style = match Ppstyle.get_style_format tag with
       | None    -> empty
       | Some st -> st
     in
@@ -156,7 +156,7 @@ let init_color_output () =
   let open Pp_control in
   let push_tag, pop_tag, clear_tag = make_style_stack () in
   std_logger_cleanup := clear_tag;
-  std_logger_tag     := Some Ppstyle.pp_tag;
+  std_logger_tag     := Some Ppstyle.to_format;
   let tag_handler = {
     Format.mark_open_tag   = push_tag;
     Format.mark_close_tag  = pop_tag;
diff --git a/lib/pp.ml b/lib/pp.ml
index a51b4458f..57d630a69 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -42,25 +42,7 @@ end = struct
 
 end
 
-module Tag :
-sig
-  type t 
-  type 'a key
-  val create : string -> 'a key
-  val inj : 'a -> 'a key -> t
-  val prj : t -> 'a key -> 'a option
-end =
-struct
-
-module Dyn = Dyn.Make(struct end)
-
-type t = Dyn.t
-type 'a key = 'a Dyn.tag
-let create = Dyn.create
-let inj = Dyn.Easy.inj
-let prj = Dyn.Easy.prj
-
-end
+type pp_tag = string list
 
 open Pp_control
 
@@ -95,7 +77,7 @@ type 'a ppcmd_token =
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_comment of string list
-  | Ppcmd_open_tag of Tag.t
+  | Ppcmd_open_tag of pp_tag
   | Ppcmd_close_tag
 
 type 'a ppdir_token =
@@ -243,7 +225,7 @@ let rec pr_com ft s =
       Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
-type tag_handler = Tag.t -> Format.tag
+type tag_handler = pp_tag -> Format.tag
 
 (* pretty printing functions *)
 let pp_dirs ?pp_tag ft =
diff --git a/lib/pp.mli b/lib/pp.mli
index f17908262..64ebea196 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -67,27 +67,11 @@ val close : unit -> std_ppcmds
 
 (** {6 Opening and closing of tags} *)
 
-module Tag :
-sig
-  type t
-  (** Type of tags. Tags are dynamic types comparable to {Dyn.t}. *)
+(* XXX: Improve and add attributes *)
+type pp_tag = string list
 
-  type 'a key
-  (** Keys used to inject tags *)
-
-  val create : string -> 'a key
-  (** Create a key with the given name. Two keys cannot share the same name, if
-      ever this is the case this function raises an assertion failure. *)
-
-  val inj : 'a -> 'a key -> t
-  (** Inject an object into a tag. *)
-
-  val prj : t -> 'a key -> 'a option
-  (** Project an object from a tag. *)
-end
-
-val tag : Tag.t -> std_ppcmds -> std_ppcmds
-val open_tag : Tag.t -> std_ppcmds
+val tag : pp_tag -> std_ppcmds -> std_ppcmds
+val open_tag : pp_tag -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
 (** {6 Utilities} *)
@@ -165,7 +149,7 @@ val pr_loc : Loc.t -> std_ppcmds
 (** {6 Low-level pretty-printing functions with and without flush} *)
 
 (** FIXME: These ignore the logging settings and call [Format] directly *)
-type tag_handler = Tag.t -> Format.tag
+type tag_handler = pp_tag -> Format.tag
 
 (** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
 val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index aa47c5167..298e3be6b 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -8,32 +8,38 @@
 
 module String = CString
 
-type t = string
-(** We use the concatenated string, with dots separating each string. We
-    forbid the use of dots in the strings. *)
+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 check s = if String.contains s '.' then invalid_arg "Ppstyle.make" in
-  let () = List.iter check tag in
-  let name = String.concat "." tag in
+  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 () = tags := String.Map.add name style !tags  in
+  tag
 
-let repr t = String.split '.' t
+let repr t = t
 
 let get_style tag =
-  try String.Map.find tag !tags with Not_found -> assert false
+  try String.Map.find (to_format tag) !tags
+  with Not_found -> assert false
+
+let get_style_format 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
+  try tags := String.Map.update (to_format 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 dump () =
+  List.map (fun (s,b) -> (String.split '.' s, b)) (String.Map.bindings !tags)
 
 let parse_config s =
   let styles = Terminal.parse s in
@@ -42,8 +48,6 @@ let parse_config s =
   in
   tags := List.fold_left set !tags styles
 
-let tag = Pp.Tag.create "ppstyle"
-
 (** Default tag is to reset everything *)
 let default = Terminal.({
   fg_color = Some `DEFAULT;
@@ -67,7 +71,3 @@ let warning_tag =
 let debug_tag =
   let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in
   make ~style ["message"; "debug"]
-
-let pp_tag t = match Pp.Tag.prj t tag with
-| None -> ""
-| Some key -> key
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index d9fd75765..b9422f7cf 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -11,7 +11,11 @@
 
 (** {5 Style tags} *)
 
-type t = string
+(** This API is provisional and will likely be refined. *)
+type t = Pp.pp_tag
+
+val to_format : t -> Format.tag
+val of_format : Format.tag -> t
 
 (** Style tags *)
 
@@ -23,14 +27,15 @@ val repr : t -> string list
 (** Gives back the original name of the style tag where each string has been
     concatenated and separated with a dot. *)
 
-val tag : t Pp.Tag.key
-(** An annotation for styles *)
-
 (** {5 Manipulating global styles} *)
 
 val get_style : t -> Terminal.style option
 (** Get the style associated to a tag. *)
 
+val get_style_format : Format.tag -> 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. *)
 
@@ -44,13 +49,6 @@ val parse_config : string -> unit
 val dump : unit -> (t * Terminal.style option) list
 (** Recover the list of known tags together with their current style. *)
 
-(** {5 Color output} *)
-
-val pp_tag : Pp.tag_handler
-(** Returns the name of a style tag that is understandable by the formatters
-    that have been inititialized through {!init_color_output}. To be used with
-    {!Pp.pp_with}. *)
-
 (** {5 Tags} *)
 
 val error_tag : t
diff --git a/lib/richpp.ml b/lib/richpp.ml
index d1c6d158e..c0128dbc2 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -177,10 +177,7 @@ let richpp_of_xml xml = xml
 let richpp_of_string s = PCData s
 
 let richpp_of_pp pp =
-  let annotate t = match Pp.Tag.prj t Ppstyle.tag with
-  | None -> None
-  | Some key -> Some (Ppstyle.repr key)
-  in
+  let annotate t = Some (Ppstyle.repr t)    in
   let rec drop = function
   | PCData s -> [PCData s]
   | Element (_, annotation, cs) ->
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 287d265a8..2e839e996 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -22,7 +22,7 @@ type 'annotation located = {
     The [get_annotations] function is used to convert tags into the desired
     annotation. *)
 val rich_pp :
-  (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds ->
+  (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds ->
   'annotation located Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 72bd11e03..a637d2e43 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -105,7 +105,7 @@ module Error = struct
              Printf.sprintf "Unsupported Unicode character (0x%x)" x)
 
   (* Require to fix the Camlp4 signature *)
-  let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x))
+  let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.to_format ppf (Pp.str (to_string x))
 
 end
 open Error
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 9dacce28d..d9410a088 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -43,7 +43,7 @@ struct
 
 end
 
-let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+let tag t s = Pp.tag t s
 let do_not_tag _ x = x
 let tag_keyword                 = tag Tag.keyword
 let tag_primitive               = tag Tag.primitive
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index b16384c60..c772f7be1 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -52,7 +52,7 @@ struct
 end
 
 let do_not_tag _ x = x
-let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+let tag t s = Pp.tag t s
 let tag_keyword     = tag Tag.keyword
 let tag_evar        = tag Tag.evar
 let tag_type        = tag Tag.univ
diff --git a/printing/printmod.ml b/printing/printmod.ml
index dfa66d437..ac7ff7697 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -26,6 +26,20 @@ open Goptions
     the "short" mode or (Some env) in the "rich" one.
 *)
 
+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"]
+end
+
+let tag t s = Pp.tag t s
+let tag_definition s = tag Tag.definition s
+let tag_keyword s = tag Tag.keyword s
+
 let short = ref false
 
 let _ =
@@ -44,14 +58,8 @@ let mk_fake_top =
   let r = ref 0 in
   fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
 
-module Make (Taggers : sig
-  val tag_definition : std_ppcmds -> std_ppcmds
-  val tag_keyword : std_ppcmds -> std_ppcmds
-end) =
-struct
-
-let def s = Taggers.tag_definition (str s)
-let keyword s = Taggers.tag_keyword (str s)
+let def s = tag_definition (str s)
+let keyword s = tag_keyword (str s)
 
 let get_new_id locals id =
   let rec get_id l id =
@@ -441,20 +449,4 @@ let print_modtype kn =
       with e when CErrors.noncritical e ->
 	print_signature' true None kn mtb.mod_type))
 
-end
-
-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"]
-end
 
-include Make(struct
-  let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-  let tag_definition s = tag Tag.definition s
-  let tag_keyword s = tag Tag.keyword s
-end)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0dfd06726..5521e8a40 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,7 +13,7 @@ open Flags
 open Vernac
 open Pcoq
 
-let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x
+let top_stderr x = msg_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x
 
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
@@ -309,7 +309,7 @@ let do_vernac () =
     | any ->
         let any = CErrors.push any in
         let msg = print_toplevel_error any ++ fnl () in
-        pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
+        pp_with !Pp_control.std_ft msg;
         Format.pp_print_flush !Pp_control.std_ft ()
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b73321c00..de7bc6929 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -179,7 +179,7 @@ let pp_cmd_header loc com =
    and take control of the console.
  *)
 let print_cmd_header loc com =
-  Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com);
+  Pp.pp_with ~pp_tag:Ppstyle.to_format !Pp_control.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Pp_control.std_ft ()
 
 let rec interp_vernac po chan_beautify checknav (loc,com) =
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 17897460c..148d029bc 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -47,7 +47,7 @@ let _ = CErrors.register_handler explain_exn_default
 
 let wrap_vernac_error with_header (exn, info) strm =
   if with_header then
-    let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
+    let header = Pp.tag Ppstyle.error_tag (str "Error:") in
     let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
     (e, info)
   else