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.

1 files changed, 6 insertions, 8 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