check_for_interrupt: better (but slower) in threading mode

Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.

2 files changed, 5 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0f118a7c6d..a36d2675d6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -230,6 +230,8 @@ let catchable_exception = function
 (* Unit of the tactic monad *)
 let tclUNIT a = (Proof.ret a:'a Proof.t)
 
+let tclCHECKINTERRUPT a = Control.check_for_interrupt (); Proof.ret a
+
 (* Bind operation of the tactic monad *)
 let tclBIND = Proof.bind
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index affe276800..0c75eb5aff 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -139,6 +139,9 @@ val apply : Environ.env -> 'a tactic -> proofview -> 'a
 
 (* Unit of the tactic monad *)
 val tclUNIT : 'a -> 'a tactic
+ 
+(* Unit but checks for interrupts *) 
+val tclCHECKINTERRUPT : 'a -> 'a tactic
 
 (* Bind operation of the tactic monad *)
 val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic