coq

Formal proof management system
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library coqide-server.protocol
Module Xmlprotocol
type 'a call
type unknown_call =
| Unknown : 'a call -> unknown_call
val abstract_eval_call : Interface.handler -> 'a call -> bool * 'a Interface.value

* Protocol version

val protocol_version : string
type msg_format =
| Richpp of {
width : int;
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

val of_call : 'a call -> Xml_datatype.xml
val of_answer : msg_format -> 'a call -> 'a Interface.value -> Xml_datatype.xml
val to_answer : 'a call -> Xml_datatype.xml -> 'a Interface.value
val document : ( Xml_datatype.xml -> string ) -> unit

* Debug printing

val pr_call : 'a call -> string
val pr_value : 'a Interface.value -> string
val pr_full_value : 'a call -> 'a Interface.value -> string
type msg_type =
| Feedback
| LtacDebugInfo
| Other

Classification of messages handled by different mechanisms

val msg_kind : Xml_datatype.xml -> msg_type

* Serialization of feedback

val to_feedback : Xml_datatype.xml -> Feedback.feedback
val of_ltac_debug_answer : tag:string -> Pp.t -> Xml_datatype.xml

* Serialization of debugger output

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

* reply for db_vars message

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

* reply for db_stack message