1 files changed, 122 insertions, 3 deletions

diff --git a/toplevel/interface.mli b/toplevel/interface.mli
index 7b4312a3..f2a22f22 100644
--- a/toplevel/interface.mli
+++ b/toplevel/interface.mli
@@ -86,8 +86,8 @@ type search_constraint =
     the flag should be negated. *)
 type search_flags = (search_constraint * bool) list
 
-(** A named object in Coq. [coq_object_qualid] is the shortest path defined for 
-    the user. [coq_object_prefix] is the missing part to recover the fully 
+(** A named object in Coq. [coq_object_qualid] is the shortest path defined for
+    the user. [coq_object_prefix] is the missing part to recover the fully
     qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
     [coq_object_object] is the actual content of the object. *)
 type 'a coq_object = {
@@ -103,10 +103,129 @@ type coq_info = {
   compile_date : string;
 }
 
-(** * Coq answers to CoqIde *)
+(** Coq unstructured messages *)
+
+type message_level =
+  | Debug of string
+  | Info
+  | Notice
+  | Warning
+  | Error
+
+type message = {
+  message_level : message_level;
+  message_content : string;
+}
+
+(** Coq "semantic" infos obtained during parsing/execution *)
+type edit_id = int
+
+type feedback_content =
+  | AddedAxiom
+  | Processed
+  | GlobRef of (int*int) * string * string * string * string
+
+type feedback = {
+  edit_id : edit_id;
+  content : feedback_content;
+}
+
+(** Calls result *)
 
 type location = (int * int) option (* start and end of the error *)
 
 type 'a value =
   | Good of 'a
   | Fail of (location * string)
+
+(* Request/Reply message protocol between Coq and CoqIde *)
+
+(** Running a command (given as its id and its text).
+    "raw" mode (less sanity checks, no impact on the undo stack)
+    is suitable for queries, or for the Set/Unset
+    of display options that coqide performs all the time.
+    The returned string contains the messages produced
+    but not the updated goals (they are
+    to be fetch by a separated [current_goals]). *)
+type interp_sty = edit_id * raw * verbose * string
+type interp_rty = string
+
+(** Backtracking by at least a certain number of phrases.
+    No finished proofs will be re-opened. Instead,
+    we continue backtracking until before these proofs,
+    and answer the amount of extra backtracking performed.
+    Backtracking by more than the number of phrases already
+    interpreted successfully (and not yet undone) will fail. *)
+type rewind_sty = int
+type rewind_rty = int
+
+(** Fetching the list of current goals. Return [None] if no proof is in
+    progress, [Some gl] otherwise. *)
+type goals_sty = unit
+type goals_rty = goals option
+
+(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+    proof is in progress. *)
+type evars_sty = unit
+type evars_rty = evar list option
+
+(** Retrieving the tactics applicable to the current goal. [None] if there is
+    no proof in progress. *)
+type hints_sty = unit
+type hints_rty = (hint list * hint) option
+
+(** The status, for instance "Ready in SomeSection, proving Foo" *)
+type status_sty = unit
+type status_rty = status
+
+(** Search for objects satisfying the given search flags. *)
+type search_sty = search_flags
+type search_rty = string coq_object list
+
+(** Retrieve the list of options of the current toplevel *)
+type get_options_sty = unit
+type get_options_rty = (option_name * option_state) list
+
+(** Set the options to the given value. Warning: this is not atomic, so whenever
+    the call fails, the option state can be messed up... This is the caller duty
+    to check that everything is correct. *)
+type set_options_sty = (option_name * option_value) list
+type set_options_rty = unit
+
+(** Is a directory part of Coq's loadpath ? *)
+type inloadpath_sty = string
+type inloadpath_rty = bool
+
+(** Create a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables. *)
+type mkcases_sty = string
+type mkcases_rty = string list list
+
+(** Quit gracefully the interpreter. *)
+type quit_sty = unit
+type quit_rty = unit
+
+type about_sty = unit
+type about_rty = coq_info
+
+type handle_exn_rty = location * string
+type handle_exn_sty = exn
+
+type handler = {
+  interp      : interp_sty      -> interp_rty;
+  rewind      : rewind_sty      -> rewind_rty;
+  goals       : goals_sty       -> goals_rty;
+  evars       : evars_sty       -> evars_rty;
+  hints       : hints_sty       -> hints_rty;
+  status      : status_sty      -> status_rty;
+  search      : search_sty      -> search_rty;
+  get_options : get_options_sty -> get_options_rty;
+  set_options : set_options_sty -> set_options_rty;
+  inloadpath  : inloadpath_sty  -> inloadpath_rty;
+  mkcases     : mkcases_sty     -> mkcases_rty;
+  quit        : quit_sty        -> quit_rty;
+  about       : about_sty       -> about_rty;
+  handle_exn  : handle_exn_sty  -> handle_exn_rty;
+}
+