aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.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/feedback.ml
parent85fca507c6c4810d0858d6fbd8f5a1ece52e755c (diff)
Rich printing of messages.
Diffstat (limited to 'lib/feedback.ml')
-rw-r--r--lib/feedback.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml
index a5e16ea04..1726da2fd 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -18,7 +18,7 @@ type message_level =
type message = {
message_level : message_level;
- message_content : string;
+ message_content : xml;
}
let of_message_level = function
@@ -39,12 +39,12 @@ let to_message_level =
let of_message msg =
let lvl = of_message_level msg.message_level in
- let content = Serialize.of_string msg.message_content in
+ let content = Serialize.of_xml msg.message_content in
Xml_datatype.Element ("message", [], [lvl; content])
let to_message xml = match xml with
| Xml_datatype.Element ("message", [], [lvl; content]) -> {
message_level = to_message_level lvl;
- message_content = Serialize.to_string content }
+ message_content = Serialize.to_xml content }
| _ -> raise Serialize.Marshal_error
let is_message = function