diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-05 13:40:29 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:47:47 -0400 |
| commit | c4789644ab4d1a88f1331efb29b69011a30f5eed (patch) | |
| tree | e1015dc4133cd066dc90fcc3b406f53ef7b771bb | |
| parent | 5e2bf8c82d08327044074330dff958fd32a8bcde (diff) | |
xmlprotocol: fix unmarshaling of Feedback.Message
| -rw-r--r-- | ide/xmlprotocol.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index a4f133810..a55d19aa1 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -788,6 +788,10 @@ let of_message lvl msg = let lvl = of_message_level lvl in let content = of_richpp msg in Xml_datatype.Element ("message", [], [lvl; content]) +let to_message xml = match xml with + | Xml_datatype.Element ("message", [], [lvl; content]) -> + Message(to_message_level lvl, to_richpp content) + | x -> raise (Marshal_error("message",x)) let is_message = function | Xml_datatype.Element ("message", [], [lvl; content]) -> @@ -816,8 +820,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> FileLoaded (to_string dirpath, to_string filename) - | "message", [lvl; content] -> - Message (to_message_level lvl, to_richpp content) + | "message", [x] -> to_message x | x,l -> raise (Marshal_error("feedback_content",PCData (x ^ " with attributes " ^ string_of_int (List.length l))))) let of_feedback_content = function |