aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/control.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-10 04:27:21 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-11 12:43:25 +0100
commit50159f9c1748ccf1d66341d171081a998d116d2f (patch)
treeef58c58b10abcb45142b56d261bc15f034b2731e /lib/control.ml
parenta758aac39aa330911f5f589ab3cae1bebed1e9ce (diff)
[flags] [stm] Reorganize flags.
We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
Diffstat (limited to 'lib/control.ml')
-rw-r--r--lib/control.ml7
1 files changed, 2 insertions, 5 deletions
diff --git a/lib/control.ml b/lib/control.ml
index d936d7557..c6489938e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,15 +12,12 @@ let interrupt = ref false
let steps = ref 0
-let are_we_threading = lazy (
- match !Flags.async_proofs_mode with
- | Flags.APon -> true
- | _ -> false)
+let enable_thread_delay = ref false
let check_for_interrupt () =
if !interrupt then begin interrupt := false; raise Sys.Break end;
incr steps;
- if !steps = 1000 && Lazy.force are_we_threading then begin
+ if !enable_thread_delay && !steps = 1000 then begin
Thread.delay 0.001;
steps := 0;
end