From 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Jun 2016 18:51:32 +0200 Subject: [feedback] Remove unused tag on `Debug` level. IMO level indicators are not the proper place to store this information. --- ide/xmlprotocol.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index a55d19aa1b..65c85ed153 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -769,15 +769,15 @@ 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 -- cgit v1.2.3 From 893ea5219eb74aedf93bd53f23b5e050fb9acbf6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 25 Jun 2016 16:05:25 +0200 Subject: [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. --- ide/xmlprotocol.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 65c85ed153..f8f256157d 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 -- cgit v1.2.3 From 1053a1d4e8112ae78af86024073cf03c072d1a7c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 25 Jun 2016 16:14:23 +0200 Subject: [feedback] Remove `ErrorMsg` in favor of `Message Error`. The ErrorMsg datatype was introduced to allow locations in messages, however, it was redundant with error and used only in one place. We remove it in favor of a more uniform treatment of messages with location. This patch also removes the use of `Loc.ghost` in one place. Lightly tested. --- ide/xmlprotocol.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index f8f256157d..d94cb0f3ef 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -811,7 +811,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 @@ -845,8 +844,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" -- cgit v1.2.3 From a10e3e0252560992128f490dfcb3d76c4bbf317b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 25 Jun 2016 17:39:04 +0200 Subject: [xmlproto] Remove duplicated deserialization. --- ide/xmlprotocol.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'ide/xmlprotocol.ml') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d94cb0f3ef..79509fe021 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -795,10 +795,11 @@ let to_message xml = match xml with 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; xloc; content]) -> - Some (to_message_level lvl, to_option to_loc xloc, 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 -- cgit v1.2.3