From f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 28 Jun 2016 16:52:46 +0200
Subject: [ide] Use "log via feedback".

We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
---
 ide/xmlprotocol.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'ide/xmlprotocol.ml')

diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 5f82a8898b..65f44fdd38 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -795,12 +795,6 @@ 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 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
   | "processed", _ -> Processed
-- 
cgit v1.2.3