diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 11:41:40 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-18 03:44:16 +0200 |
commit | d8874dd855d748aaaf504890487ab15ffd7a677d (patch) | |
tree | bfc4b7173c489388fd650a2bd10e4e5de0719287 /stm/stm.ml | |
parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) |
[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 ####.
Diffstat (limited to 'stm/stm.ml')
-rw-r--r-- | stm/stm.ml | 23 |
1 files changed, 13 insertions, 10 deletions
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 = |