Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.

2 files changed, 15 insertions, 3 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 168d8bf084..5a34e81114 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -53,6 +53,9 @@ let execution_error, execution_error_hook = Hook.make
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
+let tactic_being_run, tactic_being_run_hook = Hook.make
+ ~default:(fun _ -> ()) ()
+
 include Hook
 
 (* enables:  Hooks.(call foo args) *)
@@ -1800,16 +1803,21 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
             reach ~cache:`Shallow view.next;
+            Hooks.(call tactic_being_run true); 
             Partac.vernac_interp
-              cancel !Flags.async_proofs_n_tacworkers view.next id x
+              cancel !Flags.async_proofs_n_tacworkers view.next id x;
+            Hooks.(call tactic_being_run false)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
             reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
-      | `Cmd { cast = x; ceff = eff } -> (fun () ->
-            reach view.next; vernac_interp id x;
+      | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
+            reach view.next;
+            if ctac then Hooks.(call tactic_being_run true); 
+            vernac_interp id x;
+            if ctac then Hooks.(call tactic_being_run false); 
 	    if eff then update_global_env ()), cache, true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             reach view.next; vernac_interp id x;
@@ -2590,4 +2598,5 @@ let interp_hook = Hooks.interp_hook
 let with_fail_hook = Hooks.with_fail_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
 let get_fix_exn () = !State.fix_exn_ref
+let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 0c05c93d4d..ad89eb71f3 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -107,6 +107,9 @@ val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
+(* called with true before and with false after a tactic explicitly
+ * in the document is run *)
+val tactic_being_run_hook : (bool -> unit) Hook.t
 
 (* Messages from the workers to the master *)
 val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t