[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`.

5 files changed, 1 insertions, 120 deletions

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. *)