diff options
| -rw-r--r-- | API/API.mli | 3 | ||||
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 4 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 9 | ||||
| -rw-r--r-- | ide/coqOps.ml | 10 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 4 | ||||
| -rw-r--r-- | ide/interface.mli | 5 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 20 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 3 | ||||
| -rw-r--r-- | stm/stm.ml | 23 | ||||
| -rw-r--r-- | stm/stm.mli | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 10 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 8 |
13 files changed, 67 insertions, 40 deletions
diff --git a/API/API.mli b/API/API.mli index 69278e7c9..b5928c023 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2266,10 +2266,9 @@ sig | VtQed of vernac_qed_type | VtProofStep of proof_step | VtProofMode of string - | VtQuery of vernac_part_of_script * report_with + | VtQuery of vernac_part_of_script * Feedback.route_id | VtStm of vernac_control * vernac_part_of_script | VtUnknown - and report_with = Stateid.t * Feedback.route_id and vernac_qed_type = Vernacexpr.vernac_qed_type = | VtKeep | VtKeepAsAxiom @@ -94,6 +94,12 @@ Build Infrastructure access to the same .cmi files. In short, use "make -j && make -j byte" instead of "make -j world byte". +XML Protocol + +- The `query` call has been modified, now it carries a mandatory + "route_id" integer parameter, that associated the result of such + query with its generated feedback. + Changes from V8.6beta1 to V8.6 ============================== diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 0728608f3..159be9a58 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -288,6 +288,10 @@ document type". This allows for a more uniform handling of printing - The legacy `Interp` call has been turned into a noop. +- The `query` call has been modified, now it carries a mandatory + "route_id" integer parameter, that associated the result of such + query with its generated feedback. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 2ff82c688..127b4a6d2 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -308,15 +308,20 @@ CoqIDE typically sets `force` to `false`. ------------------------------- +### <a name="command-query">**Query(route_id: integer, query: string, stateId: integer)**</a> + +`routeId` can be used to distinguish the result of a particular query, +`stateId` should be set to the state the query should be run. -### <a name="command-query">**Query(query: string, stateId: integer)**</a> -In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state. ```html <call val="Query"> <pair> + <route_id val="${routeId}"/> + <pair> <string>${query}</string> <state_id val="${stateId}"/> </pair> + </pair> </call> ``` #### *Returns* 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 = diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index cabd06735..538135f98 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -495,10 +495,9 @@ type vernac_type = | VtQed of vernac_qed_type | VtProofStep of proof_step | VtProofMode of string - | VtQuery of vernac_part_of_script * report_with + | VtQuery of vernac_part_of_script * Feedback.route_id | VtStm of vernac_control * vernac_part_of_script | VtUnknown -and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list diff --git a/stm/stm.ml b/stm/stm.ml index 8ca50e2d5..071d2edf9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2520,23 +2520,26 @@ let process_transaction ?(newtip=Stateid.fresh ()) anomaly(str"classifier: VtBack + VtLater must imply part_of_script.") (* Query *) - | VtQuery (false,(report_id,route)), VtNow -> - (try stm_vernac_interp report_id ~route x - with e -> - let e = CErrors.push e in - Exninfo.iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok - | VtQuery (true,(report_id,_)), w -> - assert(Stateid.equal report_id Stateid.dummy); + | VtQuery (false, route), VtNow -> + begin + let query_sid = VCS.cur_tip () in + try stm_vernac_interp (VCS.cur_tip ()) x + with e -> + let e = CErrors.push e in + Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e) + end; `Ok + | VtQuery (true, _route), w -> let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) else if Flags.(!compilation_mode = BuildVio) && VCS.((get_branch head).kind = `Master) && may_pierce_opaque x - then `SkipQueue + then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then finish (); `Ok + | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.") @@ -2766,7 +2769,7 @@ type focus = { tip : Stateid.t } -let query ~at ?(report_with=(Stateid.dummy,default_route)) s = +let query ~at ~route s = Future.purify (fun s -> if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; @@ -2779,7 +2782,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = | VtStm (w,_), _ -> ignore(process_transaction aast (VtStm (w,false), VtNow)) | _ -> - ignore(process_transaction aast (VtQuery (false,report_with), VtNow))) + ignore(process_transaction aast (VtQuery (false, route), VtNow))) s let edit_at id = diff --git a/stm/stm.mli b/stm/stm.mli index b150f9748..188b176ba 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -34,7 +34,7 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t -> throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : - at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e45..d25861d5a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -30,9 +30,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b,(id,route)) -> - "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ - " route " ^ string_of_int route + | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b @@ -92,8 +90,7 @@ let rec classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater + | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -213,7 +210,6 @@ let rec classify_vernac e = make_polymorphic res else res -let classify_as_query = - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater +let classify_as_query = VtQuery (true,Feedback.default_route), VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 932097607..4dad16fd8 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -247,16 +247,16 @@ let eval_print l coq = let to_id, need_unfocus = get_id id in after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> let to_id, _ = get_id id in - eval_call (query (phrase, to_id)) coq + eval_call (query (0,(phrase, to_id))) coq | [ Tok(_,"WAIT") ] -> let phrase = "Stm Wait." in - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"JOIN") ] -> let phrase = "Stm JoinDocument." in - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" |