diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 14:50:06 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | 678b17b52b0b59a5470d8272474e692b2fe023e3 (patch) | |
| tree | 9cae63a5e14dea376ce82c16643aeb110c95eddb /lib | |
| parent | db9b17d55f539fcfda799a9fe15caa2530cc727f (diff) | |
lib/Pp.tag: New.
A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 1 |
2 files changed, 2 insertions, 1 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 |