From 921ea3983d45051ae85b0e20bf13de2eff38e53e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 8 Feb 2017 18:13:25 +0100
Subject: [pp] Remove uses of expensive string_of_ppcmds.

In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
---
 tools/fake_ide.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 5dd2a92200..7a891239bd 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,6 +12,8 @@ let error s =
   prerr_endline ("fake_id: error: "^s);
   exit 1
 
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
 type coqtop = {
   xml_printer : Xml_printer.t;
   xml_parser : Xml_parser.t;
@@ -170,7 +172,7 @@ let print_document () =
           Str.global_replace (Str.regexp "^[\n ]*") ""
       (if String.length s > 20 then String.sub s 0 17 ^ "..."
        else s) in
-  prerr_endline (Pp.string_of_ppcmds
+  pperr_endline (
     (Document.print doc
       (fun b state_id { name; text } ->
         Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
-- 
cgit v1.2.3