From 66a245d8055923f8807ae42ed938c1d992051749 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 9 Feb 2017 03:12:18 +0100
Subject: [pp] Fix bug in richpp Format use.

Format requires a top-level box to be present, this is similar to the
fix done in `Pp.string_of_ppcmds`.
---
 ide/richpp.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ide/richpp.ml b/ide/richpp.ml
index ecf1f40211..522a3e0b31 100644
--- a/ide/richpp.ml
+++ b/ide/richpp.ml
@@ -104,9 +104,11 @@ let rich_pp width ppcmds =
 
   (** The whole output must be a valid document. To that
       end, we nest the document inside <pp> tags. *)
+  pp_open_box ft 0;
   pp_open_tag ft "pp";
   Pp.(pp_with ft ppcmds);
   pp_close_tag ft ();
+  pp_close_box ft ();
 
   (** Get the resulting XML tree. *)
   let () = pp_print_flush ft () in
-- 
cgit v1.2.3