From cdfb6705e0a2d01b7c01d83bfe898a64ee148c34 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Feb 2015 21:35:36 +0100
Subject: More efficient Richpp.

We build the rich XML at once without generating the printed string.
---
 printing/richprinter.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'printing/richprinter.ml')

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
-- 
cgit v1.2.3