[pp] Hide the internal representation of `std_ppcmds`.

Following a suggestion by @ppedrot in #390, we require `Pp` clients to
be aware that they are using a "view" on the `std_ppcmds` type.

This is not extremely useful as people caring about the documents will
indeed have to follow changes in the view, but it costs little to play
on the safe side here for now.

We also introduce a more standard notation, `Pp.t` for the main type.

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))
diff --git a/lib/pp.ml b/lib/pp.ml
index 80c599274a..9f33756dfe 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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