From edee36d00147dfaa99acf52a7b4d7ebf329b013f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 26 Jun 2014 15:37:46 +0200
Subject: 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.
---
 proofs/proofview.ml  | 2 ++
 proofs/proofview.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'proofs')

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