From f1d63425ca674f8cd9cb25eeec9f35825190162f Mon Sep 17 00:00:00 2001
From: Regis-Gianas
Date: Mon, 3 Nov 2014 10:24:25 +0100
Subject: ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate".

   - Extend the protocol with a new command called "annotate".

   - By the way, relax the dependencies between the "ide" package
     and the internal packages of Coq by *not* referring to external
     type definitions inside Interface.

     Indeed, the purpose of the protocol is to act as a barrier
     between the source tree of Coq and the source tree of Coqide.
     We should enforce this property.
     (Maybe one day coqide will be extracted from the source tree
     of Coq to live its own life.)
---
 ide/xmlprotocol.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide/xmlprotocol.mli')

diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 145c88abbf..b6677d8745 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -31,7 +31,8 @@ val init        : init_sty        -> init_rty call
 val stop_worker : stop_worker_sty -> stop_worker_rty call
 (* retrocompatibility *)
 val interp      : interp_sty      -> interp_rty call
-val print_ast      : print_ast_sty      -> print_ast_rty call
+val print_ast   : print_ast_sty   -> print_ast_rty call
+val annotate    : annotate_sty    -> annotate_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value
 
-- 
cgit v1.2.3