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 ++-- lib/feedback.ml | 6 +++--- lib/feedback.mli | 2 +- tools/fake_ide.ml | 2 +- 6 files changed, 18 insertions(+), 16 deletions(-) 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 *) diff --git a/lib/feedback.ml b/lib/feedback.ml index 12b8b27ff4..c2b512e991 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -36,8 +36,8 @@ type feedback_content = | FileLoaded of string * string (* Extra metadata *) | Custom of Loc.t * string * xml - (* Old generic messages *) - | Message of level * Richpp.richpp + (* Generic messages *) + | Message of level * Loc.t option * Richpp.richpp type feedback = { id : edit_or_state_id; @@ -142,7 +142,7 @@ let feedback ?id ?route what = let feedback_logger ?loc lvl msg = feedback ~route:!feedback_route ~id:!feedback_id - (Message (lvl, Richpp.richpp_of_pp msg)) + (Message (lvl, loc, Richpp.richpp_of_pp msg)) (* Output to file *) let ft_logger old_logger ft ?loc level mesg = diff --git a/lib/feedback.mli b/lib/feedback.mli index 7b293ae30b..36fb3867fb 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -46,7 +46,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Old generic messages *) - | Message of level * Richpp.richpp + | Message of level * Loc.t option * Richpp.richpp type feedback = { id : edit_or_state_id; (* The document part concerned *) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 221fb36d8d..8fcca535d1 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -38,7 +38,7 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop = let rec loop () = let xml = Xml_parser.parse coqtop.xml_parser in match Xmlprotocol.is_message xml with - | Some (level, content) -> + | Some (level, _loc, content) -> logger level content; loop () | None -> -- cgit v1.2.3