diff options
| -rw-r--r-- | lib/pp.ml | 4 | ||||
| -rw-r--r-- | lib/pp.mli | 27 |
2 files changed, 24 insertions, 7 deletions
@@ -19,14 +19,14 @@ open Pp_control \end{description} *) +type pp_tag = string list + type block_type = | Pp_hbox of int | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int -type pp_tag = string list - type std_ppcmds = | Ppcmd_empty | Ppcmd_string of string diff --git a/lib/pp.mli b/lib/pp.mli index f61261a17..2b2017926 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -6,9 +6,29 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Pretty-printers. *) +(** Coq document type. *) -type std_ppcmds +(* XXX: Improve and add attributes *) +type pp_tag = string list + +type block_type = + | Pp_hbox of int + | Pp_vbox of int + | Pp_hvbox of int + | Pp_hovbox of int + +type std_ppcmds = + | Ppcmd_empty + | Ppcmd_string of string + | Ppcmd_glue of std_ppcmds * std_ppcmds + | Ppcmd_box of block_type * std_ppcmds + | Ppcmd_print_break of int * int + | Ppcmd_white_space of int + | Ppcmd_force_newline + | Ppcmd_open_box of block_type + | Ppcmd_close_box + | Ppcmd_open_tag of pp_tag + | Ppcmd_close_tag (** {6 Formatting commands} *) @@ -59,9 +79,6 @@ val close : unit -> std_ppcmds (** {6 Opening and closing of tags} *) -(* XXX: Improve and add attributes *) -type pp_tag = string list - val tag : pp_tag -> std_ppcmds -> std_ppcmds val open_tag : pp_tag -> std_ppcmds val close_tag : unit -> std_ppcmds |