diff options
| -rw-r--r-- | lib/pp.ml | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 1 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 12 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 9 |
4 files changed, 7 insertions, 17 deletions
@@ -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 eb847189a..f29f9b2f3 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 ad95d9969..2039fdaa4 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 dafbc3d82..7420f2784 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 |