[ide] richpp clenaup

We remove the "abstraction breaking" primitives and reduce the file to
the used fragment.

7 files changed, 7 insertions, 45 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 88b61042e..c77232ad1 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -111,8 +111,9 @@ let annotate phrase =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  Richpp.repr (Richpp.richpp_of_pp (Ppvernac.pr_vernac ast))
-    
+  (* XXX: Width should be a parameter of annotate... *)
+  Richpp.richpp_of_pp (Ppvernac.pr_vernac ast)
+
 (** Goal display *)
 
 let hyp_next_tac sigma env decl =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 498a911ee..101f1a5ee 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -43,7 +43,7 @@ let xml_to_string xml =
   | Element (_, _, children) ->
     List.iter iter children
   in
-  let () = iter (Richpp.repr xml) in
+  let () = iter xml in
   Buffer.contents buf
 
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
@@ -75,7 +75,7 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
     let tags = try tag t :: tags with Not_found -> tags in
     List.iter (fun xml -> insert tags xml) children
   in
-  let () = try insert tags (Richpp.repr msg) with _ -> () in
+  let () = try insert tags msg with _ -> () in
   buf#delete_mark rmark
 
 let set_location = ref  (function s -> failwith "not ready")
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1ae66e23e..4b4ba72b0 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,8 +52,6 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
-val xml_to_string : Richpp.richpp -> string
-
 val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
diff --git a/ide/richpp.ml b/ide/richpp.ml
index c0128dbc2..b84c51824 100644
--- a/ide/richpp.ml
+++ b/ide/richpp.ml
@@ -172,10 +172,6 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
 
 type richpp = xml
 
-let repr xml = xml
-let richpp_of_xml xml = xml
-let richpp_of_string s = PCData s
-
 let richpp_of_pp pp =
   let annotate t = Some (Ppstyle.repr t)    in
   let rec drop = function
@@ -188,13 +184,3 @@ let richpp_of_pp pp =
   in
   let xml = rich_pp annotate pp in
   Element ("_", [], drop xml)
-
-let raw_print xml =
-  let buf = Buffer.create 1024 in
-  let rec print = function
-  | PCData s -> Buffer.add_string buf s
-  | Element (_, _, cs) -> List.iter print cs
-  in
-  let () = print xml in
-  Buffer.contents buf
-
diff --git a/ide/richpp.mli b/ide/richpp.mli
index 2e839e996..980d27407 100644
--- a/ide/richpp.mli
+++ b/ide/richpp.mli
@@ -42,23 +42,9 @@ val xml_of_rich_pp :
 
 (** {5 Enriched text} *)
 
-type richpp
+type richpp = Xml_datatype.xml
+
 (** Type of text with style annotations *)
 
 val richpp_of_pp : Pp.std_ppcmds -> richpp
 (** Extract style information from formatted text *)
-
-val richpp_of_xml : Xml_datatype.xml -> richpp
-(** Do not use outside of dedicated areas *)
-
-val richpp_of_string : string -> richpp
-(** Make a styled text out of a normal string *)
-
-val repr : richpp -> Xml_datatype.xml
-(** Observe the styled text as XML *)
-
-(** {5 Debug/Compat} *)
-
-(** Represent the semi-structured document as a string, dropping any additional
-    information. *)
-val raw_print : richpp -> string
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 08f23d3d4..6ed62082d 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]
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index f6fae24d7..43a65dfa8 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -57,10 +57,6 @@ val pr_call : 'a call -> string
 val pr_value : 'a value -> string
 val pr_full_value : 'a call -> 'a value -> string
 
-(** * Serialization of rich documents *)
-val of_richpp : Richpp.richpp -> Xml_datatype.xml
-val to_richpp : Xml_datatype.xml -> Richpp.richpp
-
 (** * Serializaiton of feedback  *)
 val of_feedback : Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback