Merge remote-tracking branch 'github/pr/223' into feedback-locations

Was PR#223: Allow feedback messages to carry a location.

6 files changed, 26 insertions, 24 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 61f002576..11621078d 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -298,7 +298,7 @@ let handle_intermediate_message handle level content =
         | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
         | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
         | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
-        | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
+        | Feedback.Debug   -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
   in
   logger level content
 
@@ -333,7 +333,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
     match Xmlprotocol.is_message xml with
-    | Some (lvl, msg) ->
+    | Some (lvl, _loc, msg) ->
       handle_intermediate_message handle lvl msg;
       loop ()
     | None ->
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6ffe771da..c912adcf1 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -460,7 +460,9 @@ object(self)
           log "GlobRef" id;
           self#attach_tooltip sentence loc
             (Printf.sprintf "%s %s %s" filepath ident ty)
-      | ErrorMsg(loc, msg), Some (id,sentence) ->
+      | Message(Error, loc, msg), Some (id,sentence) ->
+          let loc = Option.default Loc.ghost loc in
+          let msg = Richpp.raw_print msg         in
           log "ErrorMsg" id;
           remove_flag sentence `PROCESSING;
           add_flag sentence (`ERROR (loc, msg));
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 9f10b2502..86e09922c 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -472,11 +472,11 @@ let print_xml =
     with e -> let e = Errors.push e in Mutex.unlock m; iraise e
 
 
-let slave_logger xml_oc level message =
+let slave_logger xml_oc ?loc level message =
   (* convert the message into XML *)
   let msg = hov 0 message in
-  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))    in
-  let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))         in
+  let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in
   print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 00c3f88e5..f0698a54a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -301,7 +301,7 @@ type logger = Feedback.level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
-  | Feedback.Debug _ -> `DEBUG
+  | Feedback.Debug -> `DEBUG
   | Feedback.Info -> `INFO
   | Feedback.Notice -> `NOTICE
   | Feedback.Warning -> `WARNING
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index a55d19aa1..79509fe02 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -769,34 +769,37 @@ let document to_string_fmt =
 open Feedback
 
 let of_message_level = function
-  | Debug s ->
-      Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
+  | Debug ->
+      Serialize.constructor "message_level" "debug" []
   | Info -> Serialize.constructor "message_level" "info" []
   | Notice -> Serialize.constructor "message_level" "notice" []
   | Warning -> Serialize.constructor "message_level" "warning" []
   | Error -> Serialize.constructor "message_level" "error" []
 let to_message_level =
   Serialize.do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug (Serialize.raw_string args)
+  | "debug" -> Debug
   | "info" -> Info
   | "notice" -> Notice
   | "warning" -> Warning
   | "error" -> Error
   | x -> raise Serialize.(Marshal_error("error level",PCData x)))
 
-let of_message lvl msg =
+let of_message lvl loc msg =
   let lvl     = of_message_level lvl in
+  let xloc    = of_option of_loc loc in
   let content = of_richpp msg        in
-  Xml_datatype.Element ("message", [], [lvl; content])
+  Xml_datatype.Element ("message", [], [lvl; xloc; content])
+
 let to_message xml = match xml with
-  | Xml_datatype.Element ("message", [], [lvl; content]) ->
-      Message(to_message_level lvl, to_richpp content)
+  | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
+      Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
   | x -> raise (Marshal_error("message",x))
 
-let is_message = function
-  | Xml_datatype.Element ("message", [], [lvl; content]) ->
-    Some (to_message_level lvl, to_richpp content)
-  | _ -> None
+let is_message xml =
+  try begin match to_message xml with
+    | Message(l,c,m) -> Some (l,c,m)
+    | _              -> None
+  end with | Marshal_error _ -> None
 
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
@@ -809,7 +812,6 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
          to_string modpath, to_string ident, to_string ty)
   | "globdef", [loc; ident; secpath; ty] ->
        GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
-  | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
   | "inprogress", [n] -> InProgress (to_int n)
   | "workerstatus", [ns] ->
        let n, s = to_pair to_string to_string ns in
@@ -843,8 +845,6 @@ let of_feedback_content = function
         of_string ident;
         of_string secpath;
         of_string ty ]
-  | ErrorMsg(loc, s) ->
-      constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
   | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
   | WorkerStatus(n,s) ->
       constructor "feedback_content" "workerstatus"
@@ -861,7 +861,7 @@ let of_feedback_content = function
       constructor "feedback_content" "fileloaded" [
         of_string dirpath;
         of_string filename ]
-  | Message (l,m) -> constructor "feedback_content" "message" [ of_message l m ]
+  | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
 
 let of_edit_or_state_id = function
   | Edit id -> ["object","edit"], of_edit_id id
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 6bca8772e..1bb998970 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -66,7 +66,7 @@ val of_feedback : Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
 val is_feedback : xml -> bool
 
-val is_message : xml -> (Feedback.level * Richpp.richpp) option
-val of_message : Feedback.level -> Richpp.richpp -> xml
+val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option
+val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
 (* val to_message : xml -> Feedback.message *)