Passing command-line option async_proofs_worker_priority functionally.

We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".

1 files changed, 6 insertions, 6 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index fa6044fe88..909804d0c9 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -115,7 +115,7 @@ module Make(T : Task) () = struct
   type process = Worker.process
   type extra = (T.task * cancel_switch) TQueue.t
 
-  let spawn id =
+  let spawn id priority =
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
       (* Filter arguments for slaves. *)
@@ -123,7 +123,7 @@ module Make(T : Task) () = struct
         | [] -> !async_proofs_flags_for_workers @
                 ["-worker-id"; name;
                  "-async-proofs-worker-priority";
-                 CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+                 CoqworkmgrApi.(string_of_priority priority)]
         (* Options to discard: 0 arguments *)
         | "-emacs"::tl ->
           set_slave_opt tl
@@ -262,7 +262,7 @@ module Make(T : Task) () = struct
     cleaner : Thread.t option;
   }
 
-  let create size =
+  let create size priority =
     let cleaner queue =
       while true do
         try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue)
@@ -270,7 +270,7 @@ module Make(T : Task) () = struct
       done in
     let queue = TQueue.create () in
     {
-      active = Pool.create queue ~size;
+      active = Pool.create queue ~size priority;
       queue;
       cleaner = if size > 0 then Some (CThread.create cleaner queue) else None;
     }
@@ -369,8 +369,8 @@ module Make(T : Task) () = struct
      (TQueue.wait_until_n_are_waiting_then_snapshot
        (Pool.n_workers active) queue)
 
-  let with_n_workers n f =
-    let q = create n in
+  let with_n_workers n priority f =
+    let q = create n priority in
     try let rc = f q in destroy q; rc
     with e -> let e = CErrors.push e in destroy q; iraise e