From 74a5cfa8b2f1a881ebf010160421cf0775c2a084 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:49:49 +0100 Subject: Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. --- stm/stm.ml | 15 ++++++++++++--- stm/stm.mli | 3 +++ 2 files changed, 15 insertions(+), 3 deletions(-) (limited to 'stm') 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 -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- stm/asyncTaskQueue.ml | 2 +- stm/asyncTaskQueue.mli | 2 +- stm/coqworkmgrApi.ml | 2 +- stm/coqworkmgrApi.mli | 2 +- stm/dag.ml | 2 +- stm/dag.mli | 2 +- stm/lemmas.ml | 2 +- stm/lemmas.mli | 2 +- stm/proofworkertop.ml | 2 +- stm/queryworkertop.ml | 2 +- stm/spawned.ml | 2 +- stm/spawned.mli | 2 +- stm/stm.ml | 2 +- stm/tQueue.ml | 2 +- stm/tQueue.mli | 2 +- stm/tacworkertop.ml | 2 +- stm/texmacspp.ml | 2 +- stm/texmacspp.mli | 2 +- stm/vcs.ml | 2 +- stm/vcs.mli | 2 +- stm/vernac_classifier.ml | 2 +- stm/vernac_classifier.mli | 2 +- stm/vio_checking.ml | 2 +- stm/vio_checking.mli | 2 +- stm/workerPool.ml | 2 +- stm/workerPool.mli | 2 +- 26 files changed, 26 insertions(+), 26 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 222f02c007..cc97326047 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*