lib/Pp.tag: New.

   A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.

4 files changed, 7 insertions, 17 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index b8935f54dc..c47d638337 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -217,7 +217,7 @@ let tclose () = Glue.atom(Ppcmd_close_tbox)
 (* Opening and closed of tags *)
 let open_tag t = Glue.atom(Ppcmd_open_tag t)
 let close_tag () = Glue.atom(Ppcmd_close_tag)
-
+let tag t s = open_tag t ++ s ++ close_tag ()
 let eval_ppcmds l = l
 
 (* In new syntax only double quote char is escaped by repeating it *)
diff --git a/lib/pp.mli b/lib/pp.mli
index eb847189a3..f29f9b2f3b 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -82,6 +82,7 @@ val tclose : unit -> std_ppcmds
 
 (** {6 Opening and closing of tags} *)
 
+val tag : string -> std_ppcmds -> std_ppcmds
 val open_tag : string -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ad95d99693..2039fdaa44 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -818,15 +818,9 @@ end) = struct
 
   include Make (struct
     open Ppannotation
-
-    let tag_keyword t =
-      Pp.open_tag (Indexer.index AKeyword) ++ t ++ Pp.close_tag ()
-
-    let tag_unparsing unp t =
-      Pp.open_tag (Indexer.index (AUnparsing unp)) ++ t ++ Pp.close_tag ()
-
-    let tag_constr_expr e t =
-      Pp.open_tag (Indexer.index (AConstrExpr e)) ++ t ++ Pp.close_tag ()
+    let tag_keyword       = Pp.tag (Indexer.index AKeyword)
+    let tag_unparsing unp = Pp.tag (Indexer.index (AUnparsing unp))
+    let tag_constr_expr e = Pp.tag (Indexer.index (AConstrExpr e))
   end)
 
 end
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index dafbc3d820..7420f2784e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1276,13 +1276,8 @@ end) = struct
 
   include Make (Ppconstr.RichPp (Indexer)) (struct
     open Ppannotation
-
-    let tag_keyword t =
-      Pp.open_tag (Indexer.index AKeyword) ++ t ++ Pp.close_tag ()
-
-    let tag_vernac v t =
-      Pp.open_tag (Indexer.index (AVernac v)) ++ t ++ Pp.close_tag ()
-
+    let tag_keyword  = Pp.tag (Indexer.index AKeyword)
+    let tag_vernac v = Pp.tag (Indexer.index (AVernac v))
   end)
 
 end