diff options
| -rw-r--r-- | ide/coqOps.ml | 2 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 3 | ||||
| -rw-r--r-- | lib/pp.ml | 16 | ||||
| -rw-r--r-- | lib/pp.mli | 34 |
4 files changed, 36 insertions, 19 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1b4c5d3be0..4a1d688f51 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -166,7 +166,7 @@ let flags_to_color f = else `NAME Preferences.processed_color#get (* Move to utils? *) -let rec validate (s : Pp.std_ppcmds) = match s with +let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with | Pp.Ppcmd_empty | Pp.Ppcmd_print_break _ | Pp.Ppcmd_force_newline -> true diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index b4f2ad0bef..5f80d68974 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -110,7 +110,7 @@ let to_box = let open Pp in | x -> raise (Marshal_error("*ppbox",PCData x)) ) -let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with +let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] @@ -123,6 +123,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with let rec to_pp xpp = let open Pp in + Pp.unrepr @@ do_match "ppdoc" (fun s args -> match s with | "empty" -> Ppcmd_empty | "string" -> Ppcmd_string (to_string (singleton args)) @@ -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 |