Module `Xmlprotocol`Source

* Applicative part of the interface of RocqIDE calls to Rocq

Sourcetype 'a call

Sourcetype unknown_call =

| Unknown : 'a call -> unknown_call

Sourceval add : Interface.add_sty -> Interface.add_rty call

Sourceval edit_at : Interface.edit_at_sty -> Interface.edit_at_rty call

Sourceval query : Interface.query_sty -> Interface.query_rty call

Sourceval goals : Interface.goals_sty -> Interface.goals_rty call

Sourceval hints : Interface.hints_sty -> Interface.hints_rty call

Sourceval status : Interface.status_sty -> Interface.status_rty call

Sourceval mkcases : Interface.mkcases_sty -> Interface.mkcases_rty call

Sourceval evars : Interface.evars_sty -> Interface.evars_rty call

Sourceval search : Interface.search_sty -> Interface.search_rty call

Sourceval get_options : Interface.get_options_sty -> Interface.get_options_rty call

Sourceval set_options : Interface.set_options_sty -> Interface.set_options_rty call

Sourceval quit : Interface.quit_sty -> Interface.quit_rty call

Sourceval init : Interface.init_sty -> Interface.init_rty call

Sourceval stop_worker : Interface.stop_worker_sty -> Interface.stop_worker_rty call

Sourceval wait : Interface.wait_sty -> Interface.wait_rty call

Sourceval interp : Interface.interp_sty -> Interface.interp_rty call

Sourceval print_ast : Interface.print_ast_sty -> Interface.print_ast_rty call

Sourceval annotate : Interface.annotate_sty -> Interface.annotate_rty call

Sourceval proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty call

Sourceval db_cmd : Interface.db_cmd_sty -> Interface.db_cmd_rty call

Sourceval db_upd_bpts : Interface.db_upd_bpts_sty -> Interface.db_upd_bpts_rty call

Sourceval db_continue : Interface.db_continue_sty -> Interface.db_continue_rty call

Sourceval db_stack : Interface.db_stack_sty -> Interface.db_stack_rty call

Sourceval db_vars : Interface.db_vars_sty -> Interface.db_vars_rty call

Sourceval db_configd : Interface.db_configd_sty -> Interface.db_configd_rty call

Sourceval subgoals : Interface.subgoals_sty -> Interface.subgoals_rty call

Source

val abstract_eval_call : 
  Interface.handler ->
  'a call ->
  bool * 'a Interface.value

* Protocol version

Sourceval protocol_version : string

Sourcetype msg_format =

| Richpp of {
1. width : int;
2. depth : int;
}
| Ppcmds

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

* XML data marshalling

Sourceval of_call : 'a call -> Xml_datatype.xml

Sourceval to_call : Xml_datatype.xml -> unknown_call

Sourceval of_answer : msg_format -> 'a call -> 'a Interface.value -> Xml_datatype.xml

Sourceval to_answer : 'a call -> Xml_datatype.xml -> 'a Interface.value

Sourceval document : (Xml_datatype.xml -> string) -> unit

* Debug printing

Sourceval pr_call : 'a call -> string

Sourceval pr_value : 'a Interface.value -> string

Sourceval pr_full_value : 'a call -> 'a Interface.value -> string

Sourcetype msg_type =

| Feedback
| LtacDebugInfo
| Other

Classification of messages handled by different mechanisms

Sourceval msg_kind : Xml_datatype.xml -> msg_type

Sourceval of_feedback : msg_format -> Feedback.feedback -> Xml_datatype.xml

* Serialization of feedback

Sourceval to_feedback : Xml_datatype.xml -> Feedback.feedback

Sourceval of_ltac_debug_answer : tag:string -> Pp.t -> Xml_datatype.xml

* Serialization of debugger output

Sourceval to_ltac_debug_answer : Xml_datatype.xml -> string * Pp.t

Sourceval of_vars : (string * Pp.t) list -> Xml_datatype.xml

* reply for db_vars message

Sourceval of_stack : (string * (string * int list) option) list -> Xml_datatype.xml

* reply for db_stack message

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coqide-server.protocol/Xmlprotocol/index.html

Module `Xmlprotocol`Source

package coqide-server

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coqide-server.protocol/Xmlprotocol/index.html

Module XmlprotocolSource

Module `Xmlprotocol`Source