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/coqOps.ml | 10 +++++----- ide/ide_slave.ml | 4 ++-- ide/interface.mli | 5 +++-- ide/xmlprotocol.ml | 20 +++++++++++++++++--- 4 files changed, 27 insertions(+), 12 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index d30d7ab5e..3a869f69a 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -373,7 +373,8 @@ object(self) else messages#add s; in let query = - Coq.query (phrase,sid) in + let route_id = 0 in + Coq.query (route_id,(phrase,sid)) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () | Good msg -> Coq.return () @@ -841,15 +842,14 @@ object(self) in let try_phrase phrase stop more = let action = log "Sending to coq now" in - let query = Coq.query (phrase,Stateid.dummy) in + let route_id = 0 in + let query = Coq.query (route_id,(phrase,Stateid.dummy)) in let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); messages#add (Pp.str ("Unsuccessfully tried: "^phrase)); more - | Good msg -> - messages#add_string msg; - stop Tags.Script.processed + | Good () -> stop Tags.Script.processed in Coq.bind (Coq.seq action query) next in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9c771cbef..7cb22aa33 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -109,9 +109,9 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = +let query (route, (s,id)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Stm.query ~at:id pa; "" + Stm.query ~at:id ~route pa let annotate phrase = let (loc, ast) = diff --git a/ide/interface.mli b/ide/interface.mli index 62f63aefb..1a4d6c0ec 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. *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 53eb1a95f..d42bfe43d 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20150913" +let protocol_version = "20170413" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -95,6 +95,13 @@ let to_stateid = function let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) +let to_routeid = function + | Element ("route_id",["val",i],[]) -> + let id = int_of_string i in id + | _ -> raise (Invalid_argument "to_route_id") + +let of_routeid i = Element ("route_id",["val",string_of_int i],[]) + let of_box (ppb : Pp.block_type) = let open Pp in match ppb with | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] @@ -269,6 +276,7 @@ module ReifType : sig val coq_info_t : coq_info val_t val coq_object_t : 'a val_t -> 'a coq_object val_t val state_id_t : state_id val_t + val route_id_t : route_id val_t val search_cst_t : search_constraint val_t val of_value_type : 'a val_t -> 'a -> xml @@ -304,6 +312,7 @@ end = struct | Coq_info : coq_info val_t | Coq_object : 'a val_t -> 'a coq_object val_t | State_id : state_id val_t + | Route_id : route_id val_t | Search_cst : search_constraint val_t type value_type = Value_type : 'a val_t -> value_type @@ -329,6 +338,7 @@ end = struct let coq_info_t = Coq_info let coq_object_t x = Coq_object x let state_id_t = State_id + let route_id_t = Route_id let search_cst_t = Search_cst let of_value_type (ty : 'a val_t) : 'a -> xml = @@ -350,6 +360,7 @@ end = struct | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) | Union (t1,t2) -> (of_union (convert t1) (convert t2)) | State_id -> of_stateid + | Route_id -> of_routeid | Search_cst -> of_search_cst in convert ty @@ -373,6 +384,7 @@ end = struct | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) | Union (t1,t2) -> (to_union (convert t1) (convert t2)) | State_id -> to_stateid + | Route_id -> to_routeid | Search_cst -> to_search_cst in convert ty @@ -450,6 +462,7 @@ end = struct | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id + | Route_id -> pr_int (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -475,6 +488,7 @@ end = struct | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) | State_id -> assert(true : Stateid.t exists); "Stateid.t" + | Route_id -> assert(true : route_id exists); "route_id" let print_type = function Value_type ty -> print_val_t ty @@ -506,7 +520,7 @@ open ReifType let add_sty_t : add_sty val_t = pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) let edit_at_sty_t : edit_at_sty val_t = state_id_t -let query_sty_t : query_sty val_t = pair_t string_t state_id_t +let query_sty_t : query_sty val_t = pair_t route_id_t (pair_t string_t state_id_t) let goals_sty_t : goals_sty val_t = unit_t let evars_sty_t : evars_sty val_t = unit_t let hints_sty_t : hints_sty val_t = unit_t @@ -528,7 +542,7 @@ let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) let edit_at_rty_t : edit_at_rty val_t = union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) -let query_rty_t : query_rty val_t = string_t +let query_rty_t : query_rty val_t = unit_t let goals_rty_t : goals_rty val_t = option_t goals_t let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) let hints_rty_t : hints_rty val_t = -- cgit v1.2.3