From db7b19f0f1d6b18bcc62fbedccad7a56f72315f2 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 25 Apr 2013 14:14:14 +0000 Subject: Coqide: new feedback mechanism for structured content This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/wg_Command.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'ide/wg_Command.ml') diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index e0a742779..dd8896cba 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -111,10 +111,9 @@ object(self) if String.get com (String.length com - 1) = '.' then com ^ " " else com ^ " " ^ entry#text ^" . " in - let log level message = result#buffer#insert (message^"\n") - in + let log level message = result#buffer#insert (message^"\n") in let process = - Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function + Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function | Interface.Fail (l,str) -> result#buffer#insert ("Error while interpreting "^phrase^":\n"^str); Coq.return () -- cgit v1.2.3