From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- lib/feedback.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/feedback.ml') diff --git a/lib/feedback.ml b/lib/feedback.ml index a5e16ea04c..1726da2fdb 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 -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- lib/feedback.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/feedback.ml') diff --git a/lib/feedback.ml b/lib/feedback.ml index a5e16ea04c..cce0c6bc69 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*