From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 ide/interface.mli | 55 ++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 36 insertions(+), 19 deletions(-)

(limited to 'ide/interface.mli')

diff --git a/ide/interface.mli b/ide/interface.mli
index 2a9b8b24..debbc830 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (** * Declarative part of the interface of CoqIde calls to Coq *)
@@ -12,15 +14,14 @@
 
 type raw = bool
 type verbose = bool
-type richpp = Richpp.richpp
 
 (** The type of coqtop goals *)
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : richpp list;
+  goal_hyp : Pp.t list;
   (** List of hypotheses *)
-  goal_ccl : richpp;
+  goal_ccl : Pp.t;
   (** Goal conclusion *)
 }
 
@@ -112,14 +113,17 @@ type coq_info = {
 (** Calls result *)
 
 type location = (int * int) option (* start and end of the error *)
-type state_id = Feedback.state_id
-type edit_id = Feedback.edit_id
+type state_id = Stateid.t
+type route_id = Feedback.route_id
+
+(* Obsolete *)
+type edit_id  = int
 
 (* The fail case carries the current state_id of the prover, the GUI
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * richpp)
+  | Fail of (state_id * location * Pp.t)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -128,9 +132,13 @@ type ('a, 'b) union = ('a, 'b) Util.union
 (**  [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid]
      on top of the current edit position (that is asserted to be [sid])
      verbosely if [v] is true.  The response [(id,(rc,s)] is the new state
-     [id] assigned to the phrase, some output [s].  [rc] is [Inl] if the new
+     [id] assigned to the phrase. [rc] is [Inl] if the new
      state id is the tip of the edit point, or [Inr tip] if the new phrase
-     closes a focus and [tip] is the new edit tip *)
+     closes a focus and [tip] is the new edit tip
+
+     [s] used to contain Coq's console output and has been deprecated
+     in favor of sending feedback, it will be removed in a future
+     version of the protocol.  *)
 type add_sty = (string * edit_id) * (state_id * verbose)
 type add_rty = state_id * ((unit, state_id) union * string)
 
@@ -139,21 +147,25 @@ type add_rty = state_id * ((unit, state_id) union * string)
     [Inr (start,(stop,tip))] if [id] is in a zone that can be focused.
     In that case the zone is delimited by [start] and [stop] while [tip]
     is the new document [tip].  Edits made by subsequent [add] are always
-    performend on top of [id]. *)
+    performed on top of [id]. *)
 type edit_at_sty = state_id
 type edit_at_rty = (unit, state_id * (state_id * state_id)) union
 
-(** [query s id] executes [s] at state [id] and does not record any state
-    change but for the printings that are sent in response *)
-type query_sty = string * state_id
-type query_rty = string
+(** [query s id] executes [s] at state [id].
+
+    query used to reply with the contents of Coq's console output, and
+    has been deprecated in favor of sending the query answers as
+    feedback. It will be removed in a future version of the protocol.
+*)
+type query_sty = route_id * (string * state_id)
+type query_rty = unit
 
 (** 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
+(** Retrieve the list of uninstantiated evars in the current proof. [None] if no
     proof is in progress. *)
 type evars_sty = unit
 type evars_rty = evar list option
@@ -203,7 +215,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * richpp
+type handle_exn_rty = state_id * location * Pp.t
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
@@ -219,6 +231,9 @@ type print_ast_rty = Xml_datatype.xml
 type annotate_sty = string
 type annotate_rty = Xml_datatype.xml
 
+type wait_sty = unit
+type wait_rty = unit
+
 type handler = {
   add         : add_sty         -> add_rty;
   edit_at     : edit_at_sty     -> edit_at_rty;
@@ -238,6 +253,8 @@ type handler = {
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
   init        : init_sty        -> init_rty;
   quit        : quit_sty        -> quit_rty;
+  (* for internal use (fake_id) only, do not use *)
+  wait        : wait_sty        -> wait_rty;
   (* Retrocompatibility stuff *)
   interp      : interp_sty      -> interp_rty;
 }
-- 
cgit v1.2.3