diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:14 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:14 +0000 |
commit | db7b19f0f1d6b18bcc62fbedccad7a56f72315f2 (patch) | |
tree | 42242124105af8795b5486eeade6bbbb95db55e3 /ide/coq.mli | |
parent | c4f8385b91d464e8ad0cf826eb02e4a34bbb6f15 (diff) |
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
Diffstat (limited to 'ide/coq.mli')
-rw-r--r-- | ide/coq.mli | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 0210d0b41..84ef466d7 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -63,6 +63,9 @@ val spawn_coqtop : string list -> coqtop val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit (** Register a handler called when a coqtop dies (badly or on purpose) *) +val set_feedback_handler : coqtop -> (Interface.feedback -> unit) -> unit +(** Register a handler called when coqtop sends a feedback message *) + val init_coqtop : coqtop -> unit task -> unit (** Finish initializing a freshly spawned coqtop, by running a first task on it. The task should run its inner continuation at the end. *) @@ -113,8 +116,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 interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool -> - string -> string query +val interp : + ?logger:Ideutils.logger -> + ?raw:bool -> + ?verbose:bool -> + int -> string -> string query val rewind : int -> int query val status : Interface.status query val goals : Interface.goals option query |