aboutsummaryrefslogtreecommitdiff
path: root/ide/xmlprotocol.ml
diff options
context:
space:
mode:
authorMatej Košík2017-06-11 15:14:15 +0200
committerMatej Košík2017-07-27 10:10:23 +0200
commite3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch)
treea9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /ide/xmlprotocol.ml
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'ide/xmlprotocol.ml')
-rw-r--r--ide/xmlprotocol.ml4
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