aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.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 /lib/pp.ml
parent85fca507c6c4810d0858d6fbd8f5a1ece52e755c (diff)
Rich printing of messages.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 30bc30a9a..01df2510c 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -412,7 +412,7 @@ type message_level = Feedback.message_level =
type message = Feedback.message = {
message_level : message_level;
- message_content : string;
+ message_content : Xml_datatype.xml;
}
let of_message = Feedback.of_message
@@ -511,11 +511,11 @@ let string_of_ppcmds c =
msg_with Format.str_formatter c;
Format.flush_str_formatter ()
-let log_via_feedback () = logger := (fun ~id lvl msg ->
+let log_via_feedback printer = logger := (fun ~id lvl msg ->
!feeder {
Feedback.contents = Feedback.Message {
message_level = lvl;
- message_content = string_of_ppcmds msg };
+ message_content = printer msg };
Feedback.route = !feedback_route;
Feedback.id = id })