aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-11-27 17:00:37 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-11-27 17:00:37 +0100
commit7008576175028838d5d7ba899dbc44d04e2d23c1 (patch)
treeecd6b7cfb987a08eb3a4f787b4960286b9b53a07 /stm/stm.mli
parentdae04b0020cde500fed6394b608555cad9fdb60e (diff)
STM: hook called whenever a state is unreachable
Even indirectly, if it depends on another state that in turn failed.
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 3dd0764dd..475a367b3 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -92,7 +92,7 @@ module QueryTask : AsyncTaskQueue.Task
(** customization ********************************************************** **)
(* From the master (or worker, but beware that to install the hook
- * into a worker one has to build the wroker toplevel to do so and
+ * into a worker one has to build the worker toploop to do so and
* the alternative toploop for the worker can be selected by changing
* the name of the Task(s) above) *)
@@ -100,6 +100,7 @@ val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
val parse_error_hook :
(Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> unit) Hook.t
(* Messages from the workers to the master *)
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t