[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.

2 files changed, 3 insertions, 2 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1b4c5d3be..4a1d688f5 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 b4f2ad0be..5f80d6897 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))