diff options
author | Alec Faithfull <alef@itu.dk> | 2015-10-06 13:50:59 +0200 |
---|---|---|
committer | Alec Faithfull <alef@itu.dk> | 2015-10-09 10:53:29 +0200 |
commit | b2007e86b4a28570eee52439ad8b9fee603443b8 (patch) | |
tree | 2d1fd2cb98fa75d589fb8425fed1339ce2a7514d /stm | |
parent | 73daf37ccc7a44cd29c9b67405111756c75cb26a (diff) |
STM: Pass exception information to unreachable_state_hook functions
This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
Diffstat (limited to 'stm')
-rw-r--r-- | stm/stm.ml | 4 | ||||
-rw-r--r-- | stm/stm.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index acbb5f646..e96c396ba 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -51,7 +51,7 @@ let execution_error, execution_error_hook = Hook.make feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () let unreachable_state, unreachable_state_hook = Hook.make - ~default:(fun _ -> ()) () + ~default:(fun _ _ -> ()) () include Hook @@ -736,7 +736,7 @@ end = struct (* {{{ *) let good_id = !cur_id in cur_id := Stateid.dummy; VCS.reached id false; - Hooks.(call unreachable_state id); + Hooks.(call unreachable_state id (e, info)); match Stateid.get info, safe_id with | None, None -> iraise (exn_on id ~valid:good_id (e, info)) | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info)) diff --git a/stm/stm.mli b/stm/stm.mli index 4bad7f0a6..2453f258c 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -100,7 +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 +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 |