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.
---
 ide/ide_slave.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ac38f1ea5a..f4b81a241b 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -123,7 +123,7 @@ let annotate phrase =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  let (_, _, xml) =
+  let (_, xml) =
     Richprinter.richpp_vernac ast
   in
   xml
-- 
cgit v1.2.3