Rich printing of messages.

15 files changed, 91 insertions, 66 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 8392b7dbf4..a60f327b4f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -302,13 +302,13 @@ let handle_intermediate_message handle xml =
   let logger = match handle.waiting_for with
     | Some (_, l) -> l 
     | None -> function
-        | Pp.Error -> Minilib.log ~level:`ERROR
-        | Pp.Info -> Minilib.log ~level:`INFO
-        | Pp.Notice -> Minilib.log ~level:`NOTICE
-        | Pp.Warning -> Minilib.log ~level:`WARNING
-        | Pp.Debug _ -> Minilib.log ~level:`DEBUG
+        | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s)
+        | Pp.Info -> fun s -> Minilib.log ~level:`INFO  (xml_to_string s)
+        | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
+        | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING  (xml_to_string s)
+        | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
   in
-  logger level content
+  logger level (Richpp.richpp_of_xml content)
 
 let handle_feedback feedback_processor xml =
   let feedback = Feedback.to_feedback xml in
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6a7c2e8195..80a32cc65b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -329,14 +329,14 @@ object(self)
     let display_error s =
       if not (Glib.Utf8.validate s) then
         flash_info "This error is so nasty that I can't even display it."
-      else messages#add s;
+      else messages#add_string s;
     in
     let query =
       Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
     let next = function
     | Fail (_, _, err) -> display_error err; Coq.return ()
     | Good msg ->
-      messages#add msg; Coq.return ()
+      messages#add_string msg; Coq.return ()
     in
     Coq.bind (Coq.seq action query) next
 
@@ -564,7 +564,7 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-            logger Pp.Error "You muse close the proof with Qed or Admitted";
+            logger Pp.Error (Richpp.richpp_of_string "You muse close the proof with Qed or Admitted");
             self#discard_command_queue queue;
             conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
@@ -580,7 +580,7 @@ object(self)
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Pp.Notice msg;
+                  logger Pp.Notice (Richpp.richpp_of_string msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -588,13 +588,13 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Pp.Notice msg;
+                  logger Pp.Notice (Richpp.richpp_of_string msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
               | Fail (id, loc, msg) ->
                   let sentence = Doc.pop document in
-                  self#process_interp_error queue sentence loc msg tip id in
+                  self#process_interp_error queue sentence loc (Richpp.richpp_of_string msg) tip id in
             Coq.bind coq_query handle_answer
       in
       let tip =
@@ -607,7 +607,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Pp.Info "All proof terms checked by the kernel";
+         messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
@@ -701,8 +701,8 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Pp.Error "Fixme LOC";
-          messages#push Pp.Error msg;
+          if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC");
+          messages#push Pp.Error (Richpp.richpp_of_string msg);
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
                  (Doc.focused document && Doc.is_in_focus document safe_id))
@@ -720,7 +720,7 @@ object(self)
     ?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
   =
     messages#clear;
-    messages#push Pp.Error msg;
+    messages#push Pp.Error (Richpp.richpp_of_string msg);
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
     else
@@ -779,7 +779,7 @@ object(self)
     let display_error (loc, s) =
       if not (Glib.Utf8.validate s) then
         flash_info "This error is so nasty that I can't even display it."
-      else messages#add s
+      else messages#add_string s
     in
     let try_phrase phrase stop more =
       let action = log "Sending to coq now" in
@@ -787,10 +787,10 @@ object(self)
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
-        messages#add ("Unsuccessfully tried: "^phrase);
+        messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
         more
       | Good msg ->
-        messages#add msg;
+        messages#add_string msg;
         stop Tags.Script.processed
       in
       Coq.bind (Coq.seq action query) next
@@ -834,7 +834,7 @@ object(self)
   method initialize =
     let get_initial_state =
       let next = function
-      | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
+      | Fail _ -> messages#set (Richpp.richpp_of_string "Couln't initialize Coq"); Coq.return ()
       | Good id -> initial_state <- id; Coq.return () in
       Coq.bind (Coq.init (get_filename ())) next in
     Coq.seq get_initial_state Coq.PrintOpt.enforce
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6769ce768b..e591f205f9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -318,10 +318,10 @@ let export kind sn =
         local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
-      sn.messages#set ("Running: "^cmd);
+      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
       let finally st = flash_info (cmd ^ pr_exit_status st)
       in
-      run_command sn.messages#add finally cmd
+      run_command (fun msg -> sn.messages#add_string msg) finally cmd
 
 let export kind = cb_on_current_term (export kind)
 
@@ -431,9 +431,9 @@ let compile sn =
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-      sn.messages#set ("Running: "^cmd);
+      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
       let display s =
-        sn.messages#add s;
+        sn.messages#add_string s;
         Buffer.add_string buf s
       in
       let finally st =
@@ -441,8 +441,8 @@ let compile sn =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          sn.messages#set "Compilation output:\n";
-          sn.messages#add (Buffer.contents buf);
+          sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
+          sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf));
         end
       in
       run_command display finally cmd
@@ -464,13 +464,13 @@ let make sn =
     |Some f ->
       File.saveall ();
       let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
-      sn.messages#set "Compilation output:\n";
+      sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
       Buffer.reset last_make_buf;
       last_make := "";
       last_make_index := 0;
       last_make_dir := Filename.dirname f;
       let display s =
-        sn.messages#add s;
+        sn.messages#add_string s;
         Buffer.add_string last_make_buf s
       in
       let finally st = flash_info (cmd_make#get ^ pr_exit_status st)
@@ -508,11 +508,11 @@ let next_error sn =
     let stopi = b#get_iter_at_byte ~line:(line-1) stop in
     b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
     b#place_cursor ~where:starti;
-    sn.messages#set error_msg;
+    sn.messages#set (Richpp.richpp_of_string error_msg);
     sn.script#misc#grab_focus ()
   with Not_found ->
     last_make_index := 0;
-    sn.messages#set "No more errors.\n"
+    sn.messages#set (Richpp.richpp_of_string "No more errors.\n")
 
 let next_error = cb_on_current_term next_error
 
@@ -718,7 +718,7 @@ let initial_about () =
     else ""
   in
   let msg = initial_string ^ version_info ^ log_file_message () in
-  on_current_term (fun term -> term.messages#add msg)
+  on_current_term (fun term -> term.messages#add_string msg)
 
 let coq_icon () =
   (* May raise Nof_found *)
@@ -783,7 +783,7 @@ let coqtop_arguments sn =
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
         let () = sn.messages#clear in
-        sn.messages#push Pp.Error msg
+        sn.messages#push Pp.Error (Richpp.richpp_of_string msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
@@ -1140,17 +1140,17 @@ let build_ui () =
     item "Help" ~label:"_Help";
     item "Browse Coq Manual" ~label:"Browse Coq _Manual"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add (doc_url ()));
+        browse notebook#current_term.messages#add_string (doc_url ()));
     item "Browse Coq Library" ~label:"Browse Coq _Library"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add library_url#get);
+        browse notebook#current_term.messages#add_string library_url#get);
     item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
       ~callback:(fun _ -> on_current_term (fun sn ->
-        browse_keyword sn.messages#add (get_current_word sn)));
+        browse_keyword sn.messages#add_string (get_current_word sn)));
     item "Help for μPG mode" ~label:"Help for μPG mode"
       ~callback:(fun _ -> on_current_term (fun sn ->
          sn.messages#clear;
-         sn.messages#add (NanoPG.get_documentation ())));
+         sn.messages#add_string (NanoPG.get_documentation ())));
     item "About Coq" ~label:"_About" ~stock:`ABOUT
       ~callback:MiscMenu.about
   ];
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 562de45620..414c360246 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -429,12 +429,12 @@ let print_xml =
 
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
-  let msg = string_of_ppcmds (hov 0 message) in
+  let msg = hov 0 message in
   let message = {
     Pp.message_level = level;
-    Pp.message_content = msg;
+    Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
   } in
-  let () = pr_debug (Printf.sprintf "-> %S" msg) in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
   let xml = Pp.of_message message in
   print_xml xml_oc xml
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 25cb89be3c..2e4adba735 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,6 +37,17 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
+let xml_to_string xml =
+  let open Xml_datatype in
+  let buf = Buffer.create 1024 in
+  let rec iter = function
+  | PCData s -> Buffer.add_string buf s
+  | Element (_, _, children) ->
+    List.iter iter children
+  in
+  let () = iter (Richpp.repr xml) in
+  Buffer.contents buf
+
 let translate s = s
 
 let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg =
@@ -288,7 +299,7 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Pp.message_level -> string -> unit
+type logger = Pp.message_level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
@@ -298,7 +309,7 @@ let default_logger level message =
   | Pp.Warning -> `WARNING
   | Pp.Error -> `ERROR
   in
-  Minilib.log ~level message
+  Minilib.log ~level (xml_to_string message)
 
 
 (** {6 File operations} *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index ea4c41ff0a..db2dce5a39 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,6 +52,8 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
+val xml_to_string : Richpp.richpp -> string
+
 val insert_xml : ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
@@ -67,9 +69,9 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Pp.message_level -> string -> unit
+type logger = Pp.message_level -> Richpp.richpp -> unit
 
-val default_logger : Pp.message_level -> string -> unit
+val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
 
 (** {6 I/O operations} *)
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 163bd28b13..0ae57ee748 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,7 +100,10 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message = result#buffer#insert (message^"\n") in
+      let log level message =
+        Ideutils.insert_xml result#buffer message;
+        result#buffer#insert "\n";
+      in
       let process =
 	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
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
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 457ece0900..388ab259fd 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -10,7 +10,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 type message_view =
@@ -18,9 +18,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 *)
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 8afe1cd56e..46e5d6f370 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20150815"
+let protocol_version = "20150821"
 
 (** * Interface of calls to Coq by CoqIde *)
 
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
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 52a0e9fe6f..38c867f5b5 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -18,7 +18,7 @@ type message_level =
 
 type message = {
   message_level : message_level;
-  message_content : string;
+  message_content : xml;
 }
 
 val of_message : message -> xml
diff --git a/lib/pp.ml b/lib/pp.ml
index 30bc30a9ad..01df2510cf 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 })
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 3b1123a9dc..d034e67617 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -116,7 +116,7 @@ type message_level = Feedback.message_level =
 
 type message = Feedback.message = {
   message_level : message_level;
-  message_content : string;
+  message_content : Xml_datatype.xml;
 }
 
 type logger = message_level -> std_ppcmds -> unit
@@ -154,7 +154,7 @@ val std_logger : logger
 
 val set_logger : logger -> unit
 
-val log_via_feedback : unit -> unit
+val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit
 
 val of_message : message -> Xml_datatype.xml
 val to_message : Xml_datatype.xml -> message
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index e3fb0b607a..e525031e63 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -297,7 +297,7 @@ module Make(T : Task) = struct
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback fb) []; flush oc in
     Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Pp.log_via_feedback ();
+    Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg));
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with