aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide_slave.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-21 19:00:59 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-20 15:20:32 +0200
commitf20fce1259563f2081fadc62ccab1304bb8161d5 (patch)
treeb9c63468785f5dd9f123ad9f3321bf7ed31e0455 /ide/ide_slave.ml
parent85fca507c6c4810d0858d6fbd8f5a1ece52e755c (diff)
Rich printing of messages.
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r--ide/ide_slave.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 562de4562..414c36024 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -429,12 +429,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