From b2007e86b4a28570eee52439ad8b9fee603443b8 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 13:50:59 +0200
Subject: 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
---
 stm/stm.ml  | 4 ++--
 stm/stm.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index acbb5f646d..e96c396bae 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 4bad7f0a6d..2453f258c5 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
 
-- 
cgit v1.2.3