diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-09-30 19:44:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:14 +0100 |
| commit | fd6271089a0f0fcaa6d89e347d76247c7c831d23 (patch) | |
| tree | c24377fe45b0665be9cf7de168d4e40ae105b014 /lib/pp.mli | |
| parent | 6c521565323ae8af22fb03e65664ef944da6ecdf (diff) | |
[pp] Force well-formed boxes by construction.
We replace open/close box commands in favor of the create box ones.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index ed97226ae..cee7fa052 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -22,13 +22,12 @@ type std_ppcmds = | Ppcmd_string of string | Ppcmd_glue of std_ppcmds list | Ppcmd_box of block_type * std_ppcmds + | Ppcmd_tag of pp_tag * std_ppcmds + (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_white_space of int | Ppcmd_force_newline - | Ppcmd_open_box of block_type - | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_tag of pp_tag * std_ppcmds (** {6 Formatting commands} *) @@ -69,15 +68,7 @@ val v : int -> std_ppcmds -> std_ppcmds val hv : int -> std_ppcmds -> std_ppcmds val hov : int -> std_ppcmds -> std_ppcmds -(** {6 Opening and closing of boxes} *) - -val hb : int -> std_ppcmds -val vb : int -> std_ppcmds -val hvb : int -> std_ppcmds -val hovb : int -> std_ppcmds -val close : unit -> std_ppcmds - -(** {6 Opening and closing of tags} *) +(** {6 Tagging} *) val tag : pp_tag -> std_ppcmds -> std_ppcmds |