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/wg_Command.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'ide/wg_Command.ml')

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 946aaf010d..d33c0add4a 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,12 +100,8 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message =
-        Ideutils.insert_xml result#buffer message;
-        result#buffer#insert "\n";
-      in
       let process =
-	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
+	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
             Ideutils.insert_xml result#buffer str;
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
-- 
cgit v1.2.3