[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 ####.

3 files changed, 17 insertions, 18 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 =
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