Adding a [make] primitive to the NonLogical monad.

3 files changed, 12 insertions, 0 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index bc414a7911..1ed5d92ad1 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 285cb95747..a322f8f5b5 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 07d61375ec..c2a1ff52c3 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