diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 16:05:25 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 17:17:45 +0200 |
| commit | 893ea5219eb74aedf93bd53f23b5e050fb9acbf6 (patch) | |
| tree | b1ee17d5fdbc321c30573b6c70a9c7389cf44a33 /ide | |
| parent | c9f9a159818c138af3b8d8a3a1023a66b88be207 (diff) | |
[feedback] Allow messages to carry a location.
The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.
Next step is to remove redundant MsgError feedback type.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 4 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 16 | ||||
| -rw-r--r-- | ide/xmlprotocol.mli | 4 |
3 files changed, 13 insertions, 11 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index b1f417757..86e09922c 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -475,8 +475,8 @@ let print_xml = 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/xmlprotocol.ml b/ide/xmlprotocol.ml index 65c85ed15..f8f256157 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -784,18 +784,20 @@ let to_message_level = | "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) + | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> + Some (to_message_level lvl, to_option to_loc xloc, to_richpp content) | _ -> None let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with @@ -861,7 +863,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 *) |