diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/clib.mllib | 2 | ||||
-rw-r--r-- | lib/control.ml | 16 |
2 files changed, 16 insertions, 2 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib index cd8964f02..ed4894cb9 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 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 = |