diff options
| author | Emilio Jesus Gallego Arias | 2016-11-30 22:24:17 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:38 +0100 |
| commit | 4084ee30293a6013592c0651dfeb1975711f135f (patch) | |
| tree | 5223e65acc6fe4bf92231bd728510640054aa23e /ide/xmlprotocol.ml | |
| parent | e872f76058e954fac3e0652ec567aff72226e9dd (diff) | |
[ide] richpp clenaup
We remove the "abstraction breaking" primitives and reduce the file to
the used fragment.
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 08f23d3d4e..6ed62082d7 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -92,11 +92,6 @@ let to_stateid = function let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) -let of_richpp x = Element ("richpp", [], [Richpp.repr x]) -let to_richpp xml = match xml with - | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x - | x -> raise Serialize.(Marshal_error("richpp",x)) - let of_box (ppb : Pp.block_type) = let open Pp in match ppb with | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] |