diff options
| author | Emilio Jesus Gallego Arias | 2017-03-17 18:12:03 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:51 +0100 |
| commit | fb04bc5cae0d648c379b9eb44f8b515f8e15b854 (patch) | |
| tree | 4b4f4ee083ec31e2d635ec4a4b8b7bd5cbc38adc /ide/xmlprotocol.ml | |
| parent | 66a245d8055923f8807ae42ed938c1d992051749 (diff) | |
[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.
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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)) |