Rich printing of CoqIDE protocol failure.

5 files changed, 25 insertions, 20 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 80a32cc65..8bfc70b63 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -327,9 +327,9 @@ object(self)
   method raw_coq_query phrase =
     let action = log "raw_coq_query starting now" in
     let display_error s =
-      if not (Glib.Utf8.validate s) then
+      if not (validate s) then
         flash_info "This error is so nasty that I can't even display it."
-      else messages#add_string s;
+      else messages#add s;
     in
     let query =
       Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
@@ -594,7 +594,7 @@ object(self)
                   else loop tip (List.rev topstack)
               | Fail (id, loc, msg) ->
                   let sentence = Doc.pop document in
-                  self#process_interp_error queue sentence loc (Richpp.richpp_of_string msg) tip id in
+                  self#process_interp_error queue sentence loc msg tip id in
             Coq.bind coq_query handle_answer
       in
       let tip =
@@ -702,7 +702,7 @@ object(self)
           conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC");
-          messages#push Pp.Error (Richpp.richpp_of_string msg);
+          messages#push Pp.Error 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 (Richpp.richpp_of_string msg);
+    messages#push Pp.Error msg;
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
     else
@@ -777,9 +777,9 @@ object(self)
       self#show_goals
     in
     let display_error (loc, s) =
-      if not (Glib.Utf8.validate s) then
+      if not (validate s) then
         flash_info "This error is so nasty that I can't even display it."
-      else messages#add_string s
+      else messages#add s
     in
     let try_phrase phrase stop more =
       let action = log "Sending to coq now" in
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 414c36024..c28ed6860 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -330,10 +330,14 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in
+  let mk_msg () =
+    let msg = read_stdout () in
+    let msg = str msg ++ fnl () ++ Errors.print ~info e in
+    Richpp.richpp_of_pp msg
+  in
   match e with
-  | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
-  | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
+  | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
+  | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
diff --git a/ide/interface.mli b/ide/interface.mli
index 848fb817d..f3777ba36 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -118,7 +118,7 @@ type edit_id = Feedback.edit_id
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * string)
+  | Fail of (state_id * location * richpp)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -202,7 +202,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * string
+type handle_exn_rty = state_id * location * richpp
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 0ae57ee74..7d8993aa8 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -107,7 +107,7 @@ object(self)
       let process =
 	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            result#buffer#insert str;
+            Ideutils.insert_xml result#buffer str;
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 46e5d6f37..7445ce5ca 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20150821"
+let protocol_version = "20150913"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -90,7 +90,7 @@ let of_value f = function
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
   let id = Stateid.to_xml id in
-  Element ("value", ["val", "fail"] @ loc, [id;PCData msg])
+  Element ("value", ["val", "fail"] @ loc, [id; Richpp.of_richpp msg])
 let to_value f = function
 | Element ("value", attrs, l) ->
   let ans = massoc "val" attrs in
@@ -103,8 +103,9 @@ let to_value f = function
         Some (loc_s, loc_e)
       with Marshal_error | Failure _ -> None
     in
-    let id = Stateid.of_xml (List.hd l) in
-    let msg = raw_string (List.tl l) in
+    let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in
+    let id = Stateid.of_xml id in
+    let msg = Richpp.to_richpp msg in
     Fail (id, loc, msg)
   else raise Marshal_error
 | _ -> raise Marshal_error
@@ -671,10 +672,10 @@ let to_call : xml -> unknown call =
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]"
   | Fail (id,Some(i,j),str) ->
       "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
+        " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value call value = match call with
   | Add _        -> pr_value_gen (print add_rty_t        ) (Obj.magic value)
@@ -730,7 +731,7 @@ let document to_string_fmt =
     (to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
   Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
     (to_string_fmt (of_value (fun _ -> PCData "b")
-      (Fail (Stateid.initial,Some (15,34),"error message"))));
+      (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
   document_type_encoding to_string_fmt
 
 (* vim: set foldmethod=marker: *)