diff options
Diffstat (limited to 'library/states.mli')
| -rw-r--r-- | library/states.mli | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/library/states.mli b/library/states.mli index 7e6535d92..26dec09e5 100644 --- a/library/states.mli +++ b/library/states.mli @@ -22,14 +22,20 @@ val unfreeze : state -> unit (** {6 Rollback } *) -(** [with_heavy_rollback f x] applies [f] to [x] and restores the - state of the whole system as it was before the evaluation if an exception - is raised. *) +(** [with_heavy_rollback f h x] applies [f] to [x]. If this application + ends on an exception, the wrapper [h] is applied to it, then + the state of the whole system is restored as it was before applying [f], + and finally the exception produced by [h] is raised. *) + val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b +(** [without_rollback] is just like [with_heavy_rollback], except that + no state is restored in case of exception. *) + +val without_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b + (** [with_state_protection f x] applies [f] to [x] and restores the - state of the whole system as it was before the evaluation of f *) + state of the whole system as it was before applying [f] *) val with_state_protection : ('a -> 'b) -> 'a -> 'b - |