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.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'printing/richprinter.mli')

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