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