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.
---
 lib/control.ml       | 14 ++++++--------
 proofs/proofview.ml  |  2 ++
 proofs/proofview.mli |  3 +++
 tactics/rewrite.ml   |  8 ++++++--
 tactics/tacticals.ml |  2 +-
 5 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/lib/control.ml b/lib/control.ml
index 67d5a9b4ed..18176b8433 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,18 +12,16 @@ let interrupt = ref false
 
 let steps = ref 0
 
-let slave_process =
-  let rec f = ref (fun () ->
-    match !Flags.async_proofs_mode with
-    | Flags.APonParallel n -> let b = n > 0 in f := (fun () -> b); !f ()
-    | _ -> f := (fun () -> false); !f ()) in
-  fun () -> !f ()
+let are_we_threading = lazy (
+  match !Flags.async_proofs_mode with
+  | Flags.APonParallel _ -> true
+  | _ -> false)
 
 let check_for_interrupt () =
   if !interrupt then begin interrupt := false; raise Sys.Break end;
   incr steps;
-  if !steps = 10000 && slave_process () then begin
-    Thread.yield ();
+  if !steps = 1000 && Lazy.force are_we_threading then begin
+    Thread.delay 0.001;
     steps := 0;
   end
 
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
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 171b1f75a8..2e9d30dfc4 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1213,9 +1213,13 @@ module Strategies =
 
     let try_ str : strategy = choice str id
 
+    let check_interrupt str e l c t r ev =
+      Control.check_for_interrupt ();
+      str  e l c t r ev
+    
     let fix (f : strategy -> strategy) : strategy =
-      let rec aux env = f (fun env -> aux env) env in aux
-
+      let rec aux env = f (fun env -> check_interrupt aux env) env in aux
+    
     let any (s : strategy) : strategy =
       fix (fun any -> try_ (seq s any))
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fcce6e5eba..966d355d42 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -413,7 +413,7 @@ module New = struct
   let rec tclREPEAT0 t =
     tclINDEPENDENT begin
       tclIFCATCH t
-        (fun () -> tclREPEAT0 t)
+        (fun () -> tclCHECKINTERRUPT () <*> tclREPEAT0 t)
         (fun e -> catch_failerror e <*> tclUNIT ())
     end
   let tclREPEAT t =
-- 
cgit v1.2.3