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/coq.ml | 4 ++-- ide/ideutils.ml | 2 +- ide/xmlprotocol.ml | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 61f002576b..11621078de 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/ideutils.ml b/ide/ideutils.ml index 00c3f88e56..f0698a54a3 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 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 c9f9a159818c138af3b8d8a3a1023a66b88be207 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Jun 2016 00:41:33 +0200 Subject: [feedback] Add optional ?loc parameter to loggers. This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished. --- ide/ide_slave.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9f10b2502a..b1f4177579 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -472,7 +472,7 @@ 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 -- 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/ide_slave.ml | 4 ++-- ide/xmlprotocol.ml | 16 +++++++++------- ide/xmlprotocol.mli | 4 ++-- 3 files changed, 13 insertions(+), 11 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index b1f4177579..86e09922c5 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 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 diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 6bca8772ed..1bb9989704 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 *) -- 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/coqOps.ml | 4 +++- ide/xmlprotocol.ml | 3 --- 2 files changed, 3 insertions(+), 4 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6ffe771da3..c912adcf15 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/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') 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