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

5 files changed, 23 insertions, 20 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f62065228..1101571e5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -449,9 +449,10 @@ type vernac_type =
   | VtQed of vernac_qed_type
   | VtProofStep
   | VtProofMode of string
-  | VtQuery of vernac_part_of_script
+  | VtQuery of vernac_part_of_script * report_with
   | VtStm of vernac_control * vernac_part_of_script
   | VtUnknown
+and report_with = Stateid.t (* report feedback on a different id *)
 and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 18be9b228..8ba3319de 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -783,7 +783,7 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
     [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
       add_theory id (ic t) set k cst (pre,post) power sign div]
-  | [ "Print" "Rings" ] => [Vernacexpr.VtQuery true, Vernacexpr.VtLater] -> [
+  | [ "Print" "Rings" ] => [Vernacexpr.VtQuery (true, Stateid.dummy), Vernacexpr.VtLater] -> [
     msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
       msg_notice (hov 2
@@ -1114,7 +1114,7 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
   [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
-| [ "Print" "Fields" ] => [Vernacexpr.VtQuery true, Vernacexpr.VtLater] -> [
+| [ "Print" "Fields" ] => [Vernacexpr.VtQuery (true, Stateid.dummy), Vernacexpr.VtLater] -> [
     msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
       msg_notice (hov 2
diff --git a/stm/stm.ml b/stm/stm.ml
index 455963ad5..eb1c4df1b 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 d36fd1571..3bc458f57 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 12d3a3787..dac5e5ae8 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