From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 11:41:40 +0200
Subject: [ide] Add route_id parameter to query call.

This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.

This change is necessary in order to fix bug ####.
---
 ide/interface.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'ide/interface.mli')

diff --git a/ide/interface.mli b/ide/interface.mli
index 62f63aefb9..1a4d6c0ecb 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -112,6 +112,7 @@ type coq_info = {
 
 type location = (int * int) option (* start and end of the error *)
 type state_id = Stateid.t
+type route_id = Feedback.route_id
 
 (* Obsolete *)
 type edit_id  = int
@@ -154,8 +155,8 @@ type edit_at_rty = (unit, state_id * (state_id * state_id)) union
     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 = string * state_id
-type query_rty = string
+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. *)
-- 
cgit v1.2.3