diff options
Diffstat (limited to 'lib/control.ml')
-rw-r--r-- | lib/control.ml | 16 |
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 = |