diff options
| author | Emilio Jesus Gallego Arias | 2016-06-28 16:52:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:47:13 +0100 |
| commit | f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff (patch) | |
| tree | 2a295b6855f0bab21922ea8621ee3ce680e5e7dd /ide/coq.mli | |
| 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/coq.mli')
| -rw-r--r-- | ide/coq.mli | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 8a1fa3ed15..f2876de246 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -115,15 +115,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit type 'a query = 'a Interface.value task (** A type abbreviation for coqtop specific answers *) -val add : ?logger:Ideutils.logger -> - Interface.add_sty -> Interface.add_rty query +val add : Interface.add_sty -> Interface.add_rty query val edit_at : Interface.edit_at_sty -> Interface.edit_at_rty query -val query : ?logger:Ideutils.logger -> - Interface.query_sty -> Interface.query_rty query -val status : ?logger:Ideutils.logger -> - Interface.status_sty -> Interface.status_rty query -val goals : ?logger:Ideutils.logger -> - Interface.goals_sty -> Interface.goals_rty query +val query : Interface.query_sty -> Interface.query_rty query +val status : Interface.status_sty -> Interface.status_rty query +val goals : Interface.goals_sty -> Interface.goals_rty query val evars : Interface.evars_sty -> Interface.evars_rty query val hints : Interface.hints_sty -> Interface.hints_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query |