diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml | 16 | ||||
| -rw-r--r-- | lib/pp.mli | 34 |
2 files changed, 33 insertions, 17 deletions
@@ -25,17 +25,25 @@ type block_type = | Pp_hvbox of int | Pp_hovbox of int -type std_ppcmds = +type doc_view = | Ppcmd_empty | Ppcmd_string of string - | Ppcmd_glue of std_ppcmds list - | Ppcmd_box of block_type * std_ppcmds - | Ppcmd_tag of pp_tag * std_ppcmds + | Ppcmd_glue of doc_view list + | Ppcmd_box of block_type * doc_view + | Ppcmd_tag of pp_tag * doc_view (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_force_newline | Ppcmd_comment of string list +(* Following discussion on #390, we play on the safe side and make the + internal representation opaque here. *) +type t = doc_view +type std_ppcmds = t + +let repr x = x +let unrepr x = x + (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) Rem 2 : if used for an iso8859_1 encoded string, the result is diff --git a/lib/pp.mli b/lib/pp.mli index 4b7ac5c1ae..802ffe8e7a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -10,17 +10,17 @@ (** Pretty printing guidelines ******************************************) (* *) -(* std_ppcmds is the main pretty printing datatype in he Coq. Documents *) -(* are composed laying out boxes, and users can add arbitrary metadata *) -(* that backends are free to interpret. *) +(* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type *) +(* in the Coq system. Documents are composed laying out boxes, and *) +(* users can add arbitrary tag metadata that backends are free *) (* *) -(* The datatype is public to allow serialization or advanced uses, *) -(* regular users are _strongly_ encouraged to use the top-level *) -(* functions to manipulate the type. *) +(* The datatype has a public view to allow serialization or advanced *) +(* uses, however regular users are _strongly_ warned againt its use, *) +(* they should instead rely on the available functions below. *) (* *) -(* Box order and number is indeed an important factor. Users should try *) -(* to create a proper amount of boxes. Also, the ++ operator provides *) -(* "efficient" concatenation, but directly using a list is preferred. *) +(* Box order and number is indeed an important factor. Try to create *) +(* a proper amount of boxes. The `++` operator provides "efficient" *) +(* concatenation, but using the list constructors is usually preferred. *) (* *) (* That is to say, this: *) (* *) @@ -35,23 +35,31 @@ (* XXX: Improve and add attributes *) type pp_tag = string +(* Following discussion on #390, we play on the safe side and make the + internal representation opaque here. *) +type t +type std_ppcmds = t + type block_type = | Pp_hbox of int | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int -type std_ppcmds = +type doc_view = | Ppcmd_empty | Ppcmd_string of string - | Ppcmd_glue of std_ppcmds list - | Ppcmd_box of block_type * std_ppcmds - | Ppcmd_tag of pp_tag * std_ppcmds + | Ppcmd_glue of t list + | Ppcmd_box of block_type * t + | Ppcmd_tag of pp_tag * t (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_force_newline | Ppcmd_comment of string list +val repr : std_ppcmds -> doc_view +val unrepr : doc_view -> std_ppcmds + (** {6 Formatting commands} *) val str : string -> std_ppcmds |