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.

---
 ide/wg_MessageView.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

(limited to 'ide/wg_MessageView.ml')

diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 30bb48e3f3..615e989de9 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -12,7 +12,7 @@ class type message_view_signals =
 object
   inherit GObj.misc_signals
   inherit GUtil.add_ml_signals
-  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+  method pushed : callback:Ideutils.logger -> GtkSignal.id
 end
 
 class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals =
@@ -28,9 +28,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : string -> unit
-    method set : string -> unit
-    method push : Pp.message_level -> string -> unit
+    method add : Richpp.richpp -> unit
+    method add_string : string -> unit
+    method set : Richpp.richpp -> unit
+    method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
@@ -76,14 +77,21 @@ let message_view () : message_view =
       | Pp.Warning -> [Tags.Message.warning]
       | _ -> []
       in
-      if msg <> "" then begin
-        buffer#insert ~tags msg;
-        buffer#insert ~tags "\n";
+      let rec non_empty = function
+      | Xml_datatype.PCData "" -> false
+      | Xml_datatype.PCData _ -> true
+      | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
+      in
+      if non_empty (Richpp.repr msg) then begin
+        Ideutils.insert_xml buffer ~tags msg;
+        buffer#insert (*~tags*) "\n";
         push#call (level, msg)
       end
 
     method add msg = self#push Pp.Notice msg
 
+    method add_string s = self#add (Richpp.richpp_of_string s)
+
     method set msg = self#clear; self#add msg
 
     method buffer = text_buffer
-- 
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.

---
 ide/wg_MessageView.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/wg_MessageView.ml')

diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 211db537ed..f2b8336c14 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3