[pp] Remove special tag type and handler from Pp.

For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.

We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.

This is a step towards moving the last bit of terminal code out of the
core system.

13 files changed, 37 insertions, 87 deletions

diff --git a/ide/richpp.ml b/ide/richpp.ml
index 515090f71..ecf1f4021 100644
--- a/ide/richpp.ml
+++ b/ide/richpp.ml
@@ -24,10 +24,6 @@ type 'a context = {
   (** Pending opened nodes *)
   mutable offset : int;
   (** Quantity of characters printed so far *)
-  mutable annotations : 'a option Int.Map.t;
-  (** Map associating annotations to indexes *)
-  mutable index : int;
-  (** Current index of annotations *)
 }
 
 (** We use Format to introduce tags inside the pretty-printed document.
@@ -38,23 +34,13 @@ type 'a context = {
     marking functions. As those functions are called when actually writing to
     the device, the resulting tree is correct.
 *)
-let rich_pp width annotate ppcmds =
+let rich_pp width ppcmds =
 
   let context = {
     stack = Leaf;
     offset = 0;
-    annotations = Int.Map.empty;
-    index = (-1);
   } in
 
-  let pp_tag obj =
-    let index = context.index + 1 in
-    let () = context.index <- index in
-    let obj = annotate obj in
-    let () = context.annotations <- Int.Map.add index obj context.annotations in
-    string_of_int index
-  in
-
   let pp_buffer = Buffer.create 180 in
 
   let push_pcdata () =
@@ -81,12 +67,8 @@ let rich_pp width annotate ppcmds =
     | Leaf -> assert false
     | Node (node, child, pos, ctx) ->
       let () = assert (String.equal tag node) in
-      let annotation =
-        try Int.Map.find (int_of_string node) context.annotations
-        with _ -> None
-      in
       let annotation = {
-        annotation = annotation;
+        annotation = Some tag;
         startpos = pos;
         endpos = context.offset;
       } in
@@ -123,7 +105,7 @@ let rich_pp width annotate ppcmds =
   (** The whole output must be a valid document. To that
       end, we nest the document inside <pp> tags. *)
   pp_open_tag ft "pp";
-  Pp.(pp_with ~pp_tag ft ppcmds);
+  Pp.(pp_with ft ppcmds);
   pp_close_tag ft ();
 
   (** Get the resulting XML tree. *)
@@ -173,14 +155,13 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
 type richpp = xml
 
 let richpp_of_pp width pp =
-  let annotate t = Some (Ppstyle.repr t)    in
   let rec drop = function
   | PCData s -> [PCData s]
   | Element (_, annotation, cs) ->
     let cs = List.concat (List.map drop cs) in
     match annotation.annotation with
     | None -> cs
-    | Some s -> [Element (String.concat "." s, [], cs)]
+    | Some s -> [Element (s, [], cs)]
   in
-  let xml = rich_pp width annotate pp in
+  let xml = rich_pp width pp in
   Element ("_", [], drop xml)
diff --git a/ide/richpp.mli b/ide/richpp.mli
index 0ceeeefc2..0fe4315b7 100644
--- a/ide/richpp.mli
+++ b/ide/richpp.mli
@@ -24,9 +24,7 @@ type 'annotation located = {
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
     annotation. [width] sets the printing witdh of the formatter. *)
-val rich_pp : int ->
-  (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds ->
-  'annotation located Xml_datatype.gxml
+val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
     annotations with its position in the string from which [ssdoc] is
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 6ed62082d..1d50aed03 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -112,7 +112,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with
     | Ppcmd_string s      -> constructor "ppdoc" "string" [of_string s]
     | Ppcmd_glue sl       -> constructor "ppdoc" "glue"   [of_list of_pp sl]
     | Ppcmd_box (bt,s)    -> constructor "ppdoc" "box"    [of_pair of_box of_pp (bt,s)]
-    | Ppcmd_tag (t,s)     -> constructor "ppdoc" "tag"    [of_pair (of_list of_string) of_pp (t,s)]
+    | Ppcmd_tag (t,s)     -> constructor "ppdoc" "tag"    [of_pair of_string of_pp (t,s)]
     | Ppcmd_print_break (i,j)
                           -> constructor "ppdoc" "break"     [of_pair of_int of_int (i,j)]
     | Ppcmd_force_newline -> constructor "ppdoc" "newline"   []
@@ -126,7 +126,7 @@ let rec to_pp xpp = let open Pp in
     | "glue"      -> Ppcmd_glue (to_list to_pp (singleton args))
     | "box"       -> let (bt,s) = to_pair to_box to_pp (singleton args) in
                      Ppcmd_box(bt,s)
-    | "tag"       -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in
+    | "tag"       -> let (tg,s) = to_pair to_string to_pp (singleton args) in
                      Ppcmd_tag(tg,s)
     | "break"     -> let (i,j)   = to_pair to_int to_int (singleton args) in
                      Ppcmd_print_break(i, j)
diff --git a/lib/pp.ml b/lib/pp.ml
index 5dba0356d..53c1fb4c3 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -17,7 +17,7 @@
    \end{description}
  *)
 
-type pp_tag = string list
+type pp_tag = string
 
 type block_type =
   | Pp_hbox   of int
@@ -161,10 +161,8 @@ let rec pr_com ft s =
       Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
-type tag_handler = pp_tag -> Format.tag
-
 (* pretty printing functions *)
-let pp_with ?pp_tag ft =
+let pp_with ft =
   let cpp_open_box = function
     | Pp_hbox n   -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
@@ -182,9 +180,9 @@ let pp_with ?pp_tag ft =
     | Ppcmd_print_break(m,n)  -> pp_print_break ft m n
     | Ppcmd_force_newline     -> pp_force_newline ft ()
     | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
-    | Ppcmd_tag(tag, s)       -> Option.iter (fun f -> pp_open_tag  ft (f tag)) pp_tag;
+    | Ppcmd_tag(tag, s)       -> pp_open_tag  ft tag;
                                  pp_cmd s;
-                                 Option.iter (fun _ -> pp_close_tag ft ()     ) pp_tag
+                                 pp_close_tag ft ()
   in
   try pp_cmd
   with reraise ->
@@ -197,8 +195,8 @@ let pp_with ?pp_tag ft =
    them to different windows. *)
 
 (** Output to a string formatter *)
-let string_of_ppcmds ?pp_tag c =
-  Format.fprintf Format.str_formatter "@[%a@]" (pp_with ?pp_tag) c;
+let string_of_ppcmds c =
+  Format.fprintf Format.str_formatter "@[%a@]" pp_with c;
   Format.flush_str_formatter ()
 
 (* Copy paste from Util *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 12747d3a1..ff4206534 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -33,7 +33,7 @@
 (************************************************************************)
 
 (* XXX: Improve and add attributes *)
-type pp_tag = string list
+type pp_tag = string
 
 type block_type =
   | Pp_hbox   of int
@@ -165,9 +165,7 @@ val pr_loc : Loc.t -> std_ppcmds
 
 (** {6 Main renderers, to formatter and to string } *)
 
-(** FIXME: These ignore the logging settings and call [Format] directly *)
-type tag_handler = pp_tag -> Format.tag
-
 (** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
-val pp_with          : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
-val string_of_ppcmds : ?pp_tag:tag_handler -> std_ppcmds -> string
+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
index 298e3be6b..6969c3d5c 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -19,27 +19,20 @@ 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
-  tag
-
-let repr t = t
+  name
 
 let get_style tag =
-  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 (to_format tag) st !tags
+  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 () =
-  List.map (fun (s,b) -> (String.split '.' s, b)) (String.Map.bindings !tags)
+let dump () = String.Map.bindings !tags
 
 let parse_config s =
   let styles = Terminal.parse s in
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index b9422f7cf..2690d3910 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -14,28 +14,17 @@
 (** 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 *)
 
 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. *)
 
-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. *)
-
 (** {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. *)
 
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index a637d2e43..3b84eaa81 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.to_format ppf (Pp.str (to_string x))
+  let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
 
 end
 open Error
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index b538ba1d0..5dd2a9220 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -18,7 +18,7 @@ type coqtop = {
 }
 
 let print_error msg =
-  Format.eprintf "fake_id: error: @[%a@]\n%!" (Pp.pp_with ?pp_tag:None) msg
+  Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e9506803d..43807c1ca 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -14,7 +14,7 @@ open Vernac
 open Pcoq
 
 let top_stderr x =
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
 
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 823d05580..268d40c91 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -311,18 +311,13 @@ let print_style_tags () =
   let tags = Ppstyle.dump () in
   let iter (t, st) =
     let st = match st with Some st -> st | None -> Terminal.make () in
-    let opt =
-      Terminal.eval st ^
-      String.concat "." (Ppstyle.repr 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 tags = List.map string_of_int (Terminal.repr st) in
-    let t = String.concat "." (Ppstyle.repr t) in
     Some (t ^ "=" ^ String.concat ";" tags)
   in
   let repr = List.map_filter make tags in
@@ -445,7 +440,7 @@ let get_native_name s =
     with the appropriate error code *)
 let fatal_error info anomaly =
   let msg = info ++ fnl () in
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ?pp_tag:None) msg;
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
   exit (if anomaly then 129 else 1)
 
 let parse_args arglist =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4fc4540c1..06908abb6 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -181,7 +181,7 @@ let pp_cmd_header loc com =
  *)
 (* FIXME *)
 let print_cmd_header loc com =
-  Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com);
+  Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Topfmt.std_ft ()
 
 let rec interp_vernac po chan_beautify checknav (loc,com) =
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 85981c386..e5063e27b 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -99,8 +99,8 @@ let set_margin v =
 
 type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
-let msgnl_with ?pp_tag fmt strm =
-  pp_with ?pp_tag fmt (strm ++ fnl ());
+let msgnl_with fmt strm =
+  pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
 
 (* XXX: This is really painful! *)
@@ -133,25 +133,24 @@ let make_body quoter info ?loc s =
   quoter (hov 0 (loc ++ info ++ s))
 
 (* Generic logger *)
-let gen_logger ?pp_tag dbg err ?loc level msg = match level with
-  | Debug   -> msgnl_with ?pp_tag !std_ft (make_body dbg  dbg_str ?loc msg)
-  | Info    -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg)
+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)
   (* XXX: What to do with loc here? *)
-  | Notice  -> msgnl_with ?pp_tag !std_ft msg
+  | Notice  -> msgnl_with !std_ft msg
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) ()
-  | Error   -> msgnl_with ?pp_tag !err_ft (make_body err  err_str ?loc msg)
+               msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
 
 (** Standard loggers *)
 
 (* We provide a generic clear_log_backend callback for backends
    wanting to do clenaup after the print.
 *)
-let std_logger_tag     = ref None
 let std_logger_cleanup = ref (fun () -> ())
 
 let std_logger ?loc level msg =
-  gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?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  *)
@@ -176,7 +175,7 @@ let make_style_stack () =
   | st :: _ -> st
   in
   let push tag =
-    let style = match Ppstyle.get_style_format tag with
+    let style = match Ppstyle.get_style tag with
       | None    -> empty
       | Some st -> st
     in
@@ -199,7 +198,6 @@ let make_style_stack () =
 let init_color_output () =
   let push_tag, pop_tag, clear_tag = make_style_stack () in
   std_logger_cleanup := clear_tag;
-  std_logger_tag     := Some Ppstyle.to_format;
   let tag_handler = {
     Format.mark_open_tag   = push_tag;
     Format.mark_close_tag  = pop_tag;