diff options
| author | Maxime Dénès | 2020-05-16 17:07:37 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-02 18:53:33 +0200 |
| commit | 33021618a06a94563d28691940f02a55bd9d358d (patch) | |
| tree | 9d0cab0e9ffc2f1499ec1d49b142a758d7f80fee /ide/protocol/xmlprotocol.mli | |
| parent | db768e6828af62e06eb03d36509be6f8fc1efbf3 (diff) | |
Move CoqIDE to its own folder
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
Diffstat (limited to 'ide/protocol/xmlprotocol.mli')
| -rw-r--r-- | ide/protocol/xmlprotocol.mli | 73 |
1 files changed, 0 insertions, 73 deletions
diff --git a/ide/protocol/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli deleted file mode 100644 index 44584d44d7..0000000000 --- a/ide/protocol/xmlprotocol.mli +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** * Applicative part of the interface of CoqIde calls to Coq *) - -open Interface -open Xml_datatype - -type 'a call - -type unknown_call = Unknown : 'a call -> unknown_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 -val mkcases : mkcases_sty -> mkcases_rty call -val evars : evars_sty -> evars_rty call -val search : search_sty -> search_rty call -val get_options : get_options_sty -> get_options_rty call -val set_options : set_options_sty -> set_options_rty call -val quit : quit_sty -> quit_rty call -val init : init_sty -> init_rty call -val stop_worker : stop_worker_sty -> stop_worker_rty call -(* internal use (fake_ide) only, do not use *) -val wait : wait_sty -> wait_rty call -(* retrocompatibility *) -val interp : interp_sty -> interp_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 - -(** * Protocol version *) - -val protocol_version : string - -(** By default, we still output messages in Richpp so we are - compatible with 8.6, however, 8.7 aware clients will want to - set this to Ppcmds *) -type msg_format = Richpp of int | Ppcmds - -(** * XML data marshalling *) - -val of_call : 'a call -> xml -val to_call : xml -> unknown_call - -val of_answer : msg_format -> 'a call -> 'a value -> xml -val to_answer : 'a call -> xml -> 'a value - -(* Prints the documentation of this module *) -val document : (xml -> string) -> unit - -(** * Debug printing *) - -val pr_call : 'a call -> string -val pr_value : 'a value -> string -val pr_full_value : 'a call -> 'a value -> string - -(** * Serializaiton of feedback *) -val of_feedback : msg_format -> Feedback.feedback -> xml -val to_feedback : xml -> Feedback.feedback - -val is_feedback : xml -> bool |
