From dd37aea05fd568c98eb4d3970183c3dce1c23712 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Aug 2014 23:45:30 +0200
Subject: Adding a [make] primitive to the NonLogical monad.

---
 proofs/proofview.mli       | 3 +++
 proofs/proofview_monad.ml  | 6 ++++++
 proofs/proofview_monad.mli | 3 +++
 3 files changed, 12 insertions(+)

(limited to 'proofs')

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
-- 
cgit v1.2.3