diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-09-30 17:12:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:14 +0100 |
| commit | 6c521565323ae8af22fb03e65664ef944da6ecdf (patch) | |
| tree | 78c6887c254d7dd23524e189a14434a7a5369726 /lib/pp.mli | |
| parent | 689893ab0b648c8385ce77ec47127676088fccd5 (diff) | |
[pp] Force well-tagged docs by construction.
We replace open/close tag commands by a well-balanced "tag" wrapper.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index bd8509dbc..ed97226ae 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -27,8 +27,8 @@ type std_ppcmds = | Ppcmd_force_newline | Ppcmd_open_box of block_type | Ppcmd_close_box - | Ppcmd_open_tag of pp_tag - | Ppcmd_close_tag + | Ppcmd_comment of string list + | Ppcmd_tag of pp_tag * std_ppcmds (** {6 Formatting commands} *) @@ -80,8 +80,6 @@ val close : unit -> std_ppcmds (** {6 Opening and closing of tags} *) val tag : pp_tag -> std_ppcmds -> std_ppcmds -val open_tag : pp_tag -> std_ppcmds -val close_tag : unit -> std_ppcmds (** {6 Printing combinators} *) |