From 560b24f8eab0838fd6e01da8c4373f560020aadd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 7 Jun 2014 17:04:56 +0200
Subject: Moving a Thread.yield in check_interrupt.

---
 lib/clib.mllib |  2 +-
 lib/control.ml | 16 +++++++++++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/clib.mllib b/lib/clib.mllib
index cd8964f021..ed4894cb93 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -12,11 +12,11 @@ Option
 Store
 Exninfo
 Backtrace
-Control
 IArray
 IStream
 Pp_control
 Flags
+Control
 Pp
 Deque
 CObj
diff --git a/lib/control.ml b/lib/control.ml
index 9573614fd7..8ce3334f5d 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -10,8 +10,22 @@
 
 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 check_for_interrupt () =
-  if !interrupt then begin interrupt := false; raise Sys.Break end
+  if !interrupt then begin interrupt := false; raise Sys.Break end;
+  incr steps;
+  if !steps = 10000 && slave_process () then begin
+    Thread.yield ();
+    steps := 0;
+  end
 
 (** This function does not work on windows, sigh... *)
 let unix_timeout n f e =
-- 
cgit v1.2.3