aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/control.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/control.ml')
-rw-r--r--lib/control.ml16
1 files changed, 15 insertions, 1 deletions
diff --git a/lib/control.ml b/lib/control.ml
index 9573614fd..8ce3334f5 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 =