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 +++----
 printing/richprinter.mli | 4 +---
 2 files changed, 4 insertions(+), 7 deletions(-)

(limited to 'printing')

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
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index c67d52c084..41c313514b 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -20,12 +20,10 @@
 
 (** A rich pretty-print is composed of: *)
 type rich_pp =
-    (** - a raw pretty-print ; *)
-    string
 
     (** - a generalized semi-structured document whose attributes are
         annotations ; *)
-    * Ppannotation.t Richpp.located Xml_datatype.gxml
+    Ppannotation.t Richpp.located Xml_datatype.gxml
 
     (** - an XML document, representing annotations as usual textual
         XML attributes. *)
-- 
cgit v1.2.3