diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 17:04:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 17:08:54 +0200 |
| commit | 560b24f8eab0838fd6e01da8c4373f560020aadd (patch) | |
| tree | 155efeee777cecabd7d2898da4689075129e43bc /lib | |
| parent | 24a0df63c1844c6f2c69f9644a3059d668fd1e6f (diff) | |
Moving a Thread.yield in check_interrupt.
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 = |