diff options
| author | gareuselesinge | 2013-09-30 16:09:53 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-09-30 16:09:53 +0000 |
| commit | 56c4b269dcfb724b08bbcb37e814fe97ccf034f5 (patch) | |
| tree | 358624971862250762ad18addc39acf415535a09 /lib/serialize.mli | |
| parent | 5af66c65b3a97074b95ed5434b032a651b570e98 (diff) | |
CoqIDE protocol/serialization revised
- both requests and responses are serialized using the same generic code
- no more interp message. Replaced by:
- query: performs a query (Search/Check...) at a given state
- add: adds to the document a new sentence at the current edit point
- edit_at: changes the edit point. the result could be a rewind _or_
a focus to a specific zone that can be edited without rewinding the
whole document
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16812 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/serialize.mli')
| -rw-r--r-- | lib/serialize.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/lib/serialize.mli b/lib/serialize.mli index 00e95be2ed..2b1718bf76 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -15,8 +15,9 @@ type 'a call type unknown -val interp : interp_sty -> interp_rty call -val backto : backto_sty -> backto_rty call +val add : add_sty -> add_rty call +val edit_at : edit_at_sty -> edit_at_rty call +val query : query_sty -> query_rty call val goals : goals_sty -> goals_rty call val hints : hints_sty -> hints_rty call val status : status_sty -> status_rty call @@ -51,7 +52,7 @@ val to_feedback : xml -> feedback val is_feedback : xml -> bool val of_answer : 'a call -> 'a value -> xml -val to_answer : xml -> 'a call -> 'a value +val to_answer : 'a call -> xml -> 'a value (** * Debug printing *) |