aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli3
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--stm/stm.ml21
-rw-r--r--stm/stm.mli7
-rw-r--r--stm/vernac_classifier.ml8
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 16:45:59 +0000