From 4f9ad55d1bd0a92c25316cffe8978ed0184f832d Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 23 Apr 2013 18:15:48 +0000 Subject: coqtop -compile: avoid with_heavy_rollback when non-interactive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16444 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/states.mli | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'library/states.mli') 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 - -- cgit v1.2.3