[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.

8 files changed, 27 insertions, 23 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
index ec16aa261..28c0126b4 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -176,9 +176,9 @@ let sort_cmp env univ pb s0 s1 =
         then begin
           if !Flags.debug then begin
             let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
-              (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
-               ++ Univ.pr_universes univ))
+            Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+               str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+               ++ Univ.pr_universes univ)
           end;
           raise NotConvertible
         end
diff --git a/engine/universes.ml b/engine/universes.ml
index 6720fcef8..30a9ef163 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -416,10 +416,9 @@ let constr_of_global gr =
 	(* Should be an error as we might forget constraints, allow for now
 	   to make firstorder work with "using" clauses *)
 	c
-      else raise (Invalid_argument 
-		    ("constr_of_global: globalization of polymorphic reference " ^ 
-			Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^
-			" would forget universes."))
+      else CErrors.user_err ~hdr:"constr_of_global"
+          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+	      str " would forget universes.")
     else c
 
 let constr_of_reference = constr_of_global
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index e3e1a8890..2065a4546 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -255,7 +255,7 @@ let status force =
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
   Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = t.Search.coq_object_object
+  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
 }
 
 let pattern_of_string ?env s =
diff --git a/stm/stm.ml b/stm/stm.ml
index ee142b293..b9dbb7891 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,11 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err s  = Printf.eprintf "%s] %s\n"     (System.process_id ()) s; flush stderr
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr
 
 let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
 let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
+let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else ()
+
 open Vernacexpr
 open CErrors
 open Pp
@@ -994,11 +997,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
   in
   let aux_interp cmd =
   if is_filtered_command cmd then
-    stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+    stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr)
   else match cmd with
   | VernacShow ShowScript -> ShowScript.show_script ()
   | expr ->
-    stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+    stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr);
     try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
     with e ->
       let e = CErrors.push e in
@@ -1431,11 +1434,10 @@ end = struct (* {{{ *)
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        stm_prerr_endline (fun () -> "failed with the following exception:");
-        stm_prerr_endline (fun () -> string_of_ppcmds e_msg);
+        stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
         let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
-  
+
   let perform_states query =
     if query = [] then [] else
     let is_tac e = match classify_vernac e with
@@ -1880,10 +1882,10 @@ end = struct (* {{{ *)
           let open Notations in
           try
             let pt, uc = Future.join f in
-            stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+            stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
-              str"uc=" ++ Evd.pr_evar_universe_context uc)));
+              str"uc=" ++ Evd.pr_evar_universe_context uc));
             (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
               (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
               Tactics.exact_no_check pt)
@@ -2514,7 +2516,7 @@ let reset_task_queue = Slaves.reset_task_queue
 (* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty
   ({ verbose; loc; expr } as x) c =
-  stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
   try
     let head = VCS.current_branch () in
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 5dd2a9220..7a891239b 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"
diff --git a/vernac/search.ml b/vernac/search.ml
index e1b56b131..540573843 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -367,7 +367,7 @@ let interface_search =
     let answer = {
       coq_object_prefix = prefix;
       coq_object_qualid = qualid;
-      coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
+      coq_object_object = constr;
     } in
     ans := answer :: !ans;
   in
diff --git a/vernac/search.mli b/vernac/search.mli
index c9167c485..82b79f75d 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -67,7 +67,7 @@ type 'a coq_object = {
 }
 
 val interface_search : ?glnum:int -> (search_constraint * bool) list ->
-  string coq_object list
+  constr coq_object list
 
 (** {6 Generic search function} *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 999fe297e..32e18a014 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
-let vernac_prerr_endline x =
-  if debug then prerr_endline (x ()) else ()
+(* XXX Should move to a common library *)
+let vernac_pperr_endline pp =
+  if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
 
 (* Misc *)
 
@@ -1933,7 +1934,7 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~loc locality poly c =
-  vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
      and to be put into a new doc_command datatype: *)