diff options
| author | Matej Košík | 2017-06-11 15:14:15 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-07-27 10:10:23 +0200 |
| commit | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch) | |
| tree | a9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /ide/xmlprotocol.ml | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 06c695c772..4b521a9682 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -117,7 +117,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.repr pp with +let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with | Ppcmd_empty -> constructor "ppdoc" "empty" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] @@ -149,7 +149,7 @@ let rec to_pp xpp = let open Pp in let of_richpp x = Element ("richpp", [], [x]) (* Run-time Selectable *) -let of_pp (pp : Pp.std_ppcmds) = +let of_pp (pp : Pp.t) = match !msg_format with | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) | Ppcmds -> of_pp pp |
