diff options
author | 2015-08-21 19:00:59 +0200 | |
---|---|---|
committer | 2015-09-20 15:20:32 +0200 | |
commit | f20fce1259563f2081fadc62ccab1304bb8161d5 (patch) | |
tree | b9c63468785f5dd9f123ad9f3321bf7ed31e0455 /ide/ide_slave.ml | |
parent | 85fca507c6c4810d0858d6fbd8f5a1ece52e755c (diff) |
Rich printing of messages.
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r-- | ide/ide_slave.ml | 6 |
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 |