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