STM: VtQuery holds the id of the state it refers to

3 files changed, 19 insertions, 17 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 455963ad5d..eb1c4df1bd 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1722,23 +1722,24 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
 
       (* Query *)
-      | VtQuery false, VtNow when tty = true ->
+      | VtQuery (false,report_id), VtNow when tty = true ->
           finish ();
-          (try Future.purify (vernac_interp Stateid.dummy)
+          (try Future.purify (vernac_interp report_id)
                   { verbose = true; loc; expr }
            with e when Errors.noncritical e ->
              let e = Errors.push e in
-             raise(State.exn_on Stateid.dummy e)); `Ok
-      | VtQuery false, VtNow ->
-          (try vernac_interp Stateid.dummy x
+             raise(State.exn_on report_id e)); `Ok
+      | VtQuery (false,report_id), VtNow ->
+          (try vernac_interp report_id x
            with e when Errors.noncritical e ->
              let e = Errors.push e in
-             raise(State.exn_on Stateid.dummy e)); `Ok
-      | VtQuery true, w ->
+             raise(State.exn_on report_id e)); `Ok
+      | VtQuery (true,report_id), w ->
+          assert(Stateid.equal report_id Stateid.dummy);
           let id = VCS.new_node ~id:newtip () in
           VCS.commit id (Cmd (x,[]));
           Backtrack.record (); if w == VtNow then finish (); `Ok
-      | VtQuery false, VtLater ->
+      | VtQuery (false,_), VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
 
       (* Proof *)
@@ -1840,7 +1841,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
 
 let stop_worker n = Slaves.cancel_worker n
 
-let query ~at s =
+let query ~at ?(report_with=Stateid.dummy) s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
@@ -1852,7 +1853,7 @@ let query ~at s =
          ~tty:false true (VtStm (w,false), VtNow) loc_ast)
     | _ ->
        ignore(process_transaction
-         ~tty:false true (VtQuery false, VtNow) loc_ast))
+         ~tty:false true (VtQuery (false,report_with), VtNow) loc_ast))
   s
 
 let add ~ontop ?newtip ?(check=ignore) verb eid s =
diff --git a/stm/stm.mli b/stm/stm.mli
index d36fd15717..3bc458f57f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -22,9 +22,10 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr ->
   bool -> edit_id -> string ->
     Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
-(* parses and xecutes a command at a given state, throws away its side effects
-   but for the printings *)
-val query : at:Stateid.t -> string -> unit
+(* parses and executes a command at a given state, throws away its side effects
+   but for the printings.  Feedback is sent with report_with (defaults to dummy
+   state id)  *)
+val query : at:Stateid.t -> ?report_with:Stateid.t -> string -> 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 12d3a37878..dac5e5ae88 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -20,7 +20,7 @@ let string_of_vernac_type = function
   | VtQed VtDrop -> "Qed(drop)"
   | VtProofStep -> "ProofStep"
   | VtProofMode s -> "ProofMode " ^ s
-  | VtQuery b -> "Query" ^ string_of_in_script b
+  | VtQuery (b,_) -> "Query" ^ string_of_in_script b
   | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
       "Stm" ^ string_of_in_script b
   | VtStm (VtPG, b) -> "Stm PG" ^ string_of_in_script b
@@ -42,7 +42,7 @@ let declare_vernac_classifier
 
 let elide_part_of_script_and_now (a, _) =
   match a with
-  | VtQuery _ -> VtQuery false, VtNow
+  | VtQuery (_,id) -> VtQuery (false,id), VtNow
   | VtStm (x, _) -> VtStm (x, false), VtNow
   | x -> x, VtNow
 
@@ -89,7 +89,7 @@ let rec classify_vernac e =
     | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery true, VtLater
+    | VernacCheckMayEval _ -> VtQuery (true,Stateid.dummy), VtLater
     (* ProofStep *)
     | VernacProof _ 
     | VernacBullet _ 
@@ -206,5 +206,5 @@ let rec classify_vernac e =
       make_polymorphic res
     else res
 
-let classify_as_query = VtQuery true, VtLater
+let classify_as_query = VtQuery (true,Stateid.dummy), VtLater
 let classify_as_sideeff = VtSideff [], VtLater