From 56c4b269dcfb724b08bbcb37e814fe97ccf034f5 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 30 Sep 2013 16:09:53 +0000
Subject: 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
---
 lib/serialize.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'lib/serialize.mli')

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 *)
 
-- 
cgit v1.2.3