More efficient Richpp.

We build the rich XML at once without generating the printed string.

1 files changed, 3 insertions, 4 deletions

diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d71dc82d50..d95e190749 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,21 +5,20 @@ module RichppVernac = Ppvernac.Richpp
 module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
-    string
-    * Ppannotation.t Richpp.located Xml_datatype.gxml
+    Ppannotation.t Richpp.located Xml_datatype.gxml
     * Xml_datatype.xml
 
 let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
 
 let make_richpp pr ast =
-  let raw_pp, rich_pp =
+  let rich_pp =
     rich_pp get_annotations (pr ast)
   in
   let xml = Ppannotation.(
     xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
   )
   in
-  (raw_pp, rich_pp, xml)
+  (rich_pp, xml)
 
 let richpp_vernac = make_richpp RichppVernac.pr_vernac
 let richpp_constr = make_richpp RichppConstr.pr_constr_expr