diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-28 16:52:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:13 +0100 |
| commit | f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff (patch) | |
| tree | 2a295b6855f0bab21922ea8621ee3ce680e5e7dd /ide/wg_Command.ml | |
| parent | 28d3bb3c8bddc63d038d8d55a34c928675fa9f7b (diff) | |
[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.
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 946aaf010..d33c0add4 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; |