diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-21 19:00:59 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-20 15:20:32 +0200 |
commit | f20fce1259563f2081fadc62ccab1304bb8161d5 (patch) | |
tree | b9c63468785f5dd9f123ad9f3321bf7ed31e0455 /lib/pp.ml | |
parent | 85fca507c6c4810d0858d6fbd8f5a1ece52e755c (diff) |
Rich printing of messages.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -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 }) |