1 files changed, 13 insertions, 8 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 041f2f83b8..1dcef22b91 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -184,12 +184,13 @@ let process_goal sigma g =
   let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
+    Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+  in
   let process_hyp d (env,l) =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
     let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
       (List.fold_right Environ.push_named d' env,
-       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+       (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
   let (_env, hyps) =
     Context.fold_named_list_context process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
@@ -333,10 +334,14 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in
+  let mk_msg () =
+    let msg = read_stdout () in
+    let msg = str msg ++ fnl () ++ Errors.print ~info e in
+    Richpp.richpp_of_pp msg
+  in
   match e with
-  | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
-  | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
+  | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
+  | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -432,12 +437,12 @@ let print_xml =
 
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
-  let msg = string_of_ppcmds (hov 0 message) in
+  let msg = hov 0 message in
   let message = {
     Pp.message_level = level;
-    Pp.message_content = msg;
+    Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
   } in
-  let () = pr_debug (Printf.sprintf "-> %S" msg) in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
   let xml = Pp.of_message message in
   print_xml xml_oc xml