diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:09:56 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:09:56 +0000 |
| commit | 698a1ca948794ae9509547ddabd57b5f35512f03 (patch) | |
| tree | 5d6b6c54d031a25ccc1fcdeafb37bb03416a3e34 /ide/coq.mli | |
| parent | a4b5461afbd698b148e11eae003cb4e64bc92af3 (diff) | |
CoqIDE ported to the revides protocol
- the zone to be edited is now between the marks
start_of_input and stop_of_input
- when -debug is given, the edit zone is underlined
- the cmd_stack is focused/unfocused according to the new protocol
- read only tag resurrected and used to block the "Qed" ending
a focused zone
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 330cc776f..4fe6a2188 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -122,13 +122,13 @@ 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 -> - Interface.edit_id -> string -> Interface.interp_rty query -val backto : Interface.backto_sty -> Interface.backto_rty query +val add : ?logger:Ideutils.logger -> + 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 + Interface.status_sty -> Interface.status_rty query val goals : ?logger:Ideutils.logger -> Interface.goals_sty -> Interface.goals_rty query val evars : Interface.evars_sty -> Interface.evars_rty query |