diff options
| -rw-r--r-- | proofs/proofview.mli | 3 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 3 |
3 files changed, 12 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index bc414a791..1ed5d92ad 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -496,6 +496,9 @@ module NonLogical : sig [Proof_errors.Timeout]. *) val timeout : int -> 'a t -> 'a t + (** [make f] internalize effects done by [f] in the monad. Exceptions raised + by [f] are encapsulated the same way {!raise} does it. *) + val make : (unit -> 'a) -> 'a t (* [run c] performs [c]'s side effects for real. *) val run : 'a t -> 'a diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml index 285cb9574..a322f8f5b 100644 --- a/proofs/proofview_monad.ml +++ b/proofs/proofview_monad.ml @@ -115,6 +115,12 @@ struct let timeout = fun n t -> (); fun () -> Control.timeout n t (Exception Timeout) + let make f = (); fun () -> + try f () + with e when Errors.noncritical e -> + let e = Errors.push e in + Pervasives.raise (Exception e) + let run = fun x -> try x () with Exception e as src -> let src = Errors.push src in diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index 07d61375e..c2a1ff52c 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -83,6 +83,9 @@ module NonLogical : sig val catch : 'a t -> (exn -> 'a t) -> 'a t val timeout : int -> 'a t -> 'a t + (** Construct a monadified side-effect. Exceptions raised by the argument are + wrapped with {!Exception}. *) + val make : (unit -> 'a) -> 'a t (** [run] performs effects. *) val run : 'a t -> 'a |