aboutsummaryrefslogtreecommitdiff
path: root/stm/asyncTaskQueue.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-06-10 04:27:21 +0200
committerEmilio Jesus Gallego Arias2017-12-11 12:43:25 +0100
commit50159f9c1748ccf1d66341d171081a998d116d2f (patch)
treeef58c58b10abcb45142b56d261bc15f034b2731e /stm/asyncTaskQueue.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 'stm/asyncTaskQueue.ml')
-rw-r--r--stm/asyncTaskQueue.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 28c16a656a..26aef53552 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -11,10 +11,10 @@ open Pp
open Util
let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
-
let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
type cancel_switch = bool ref
+let async_proofs_flags_for_workers = ref []
module type Task = sig
@@ -117,12 +117,12 @@ module Make(T : Task) () = struct
let name = Printf.sprintf "%s:%d" !T.name id in
let proc, ic, oc =
let rec set_slave_opt = function
- | [] -> !Flags.async_proofs_flags_for_workers @
+ | [] -> !async_proofs_flags_for_workers @
["-toploop"; !T.name^"top";
"-worker-id"; name;
"-async-proofs-worker-priority";
- Flags.string_of_priority !Flags.async_proofs_worker_priority]
- | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl
+ CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)]
+ | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
| ("-async-proofs" |"-toploop" |"-vio2vo"
|"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
|"-compile" |"-compile-verbose"