diff options
| author | Regis-Gianas | 2014-11-03 10:24:25 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | f1d63425ca674f8cd9cb25eeec9f35825190162f (patch) | |
| tree | a6784de8bf5294f707a97d9f9b4f5d9ee82e4b68 /ide/xmlprotocol.mli | |
| parent | 28a69fcd2b9d890a8242e6f1287a38abb07d8956 (diff) | |
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.)
Diffstat (limited to 'ide/xmlprotocol.mli')
| -rw-r--r-- | ide/xmlprotocol.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |