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, 8 insertions, 8 deletions

diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 15c6510f7c..f77ced2f3a 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -19,7 +19,7 @@ type 'a cpanel = {
 module type PoolModel = sig
   (* this shall come from a Spawn.* model *)
   type process
-  val spawn : int -> worker_id * process * CThread.thread_ic * out_channel
+  val spawn : int -> CoqworkmgrApi.priority -> worker_id * process * CThread.thread_ic * out_channel
 
   (* this defines the main loop of the manager *)
   type extra
@@ -79,20 +79,20 @@ let locking { lock; pool = p } f =
     x
   with e -> Mutex.unlock lock; raise e
 
-let rec create_worker extra pool id =
+let rec create_worker extra pool priority id =
   let cancel = ref false in
-  let name, process, ic, oc as worker = Model.spawn id in
+  let name, process, ic, oc as worker = Model.spawn id priority in
   master_handshake name ic oc;
-  let exit () = cancel := true; cleanup pool; Thread.exit () in
+  let exit () = cancel := true; cleanup pool priority; Thread.exit () in
   let cancelled () = !cancel in
   let cpanel = { exit; cancelled; extra } in
   let manager = CThread.create (Model.manager cpanel) worker in
   { name; cancel; manager; process }
   
-and cleanup x = locking x begin fun { workers; count; extra_arg } ->
+and cleanup x priority = locking x begin fun { workers; count; extra_arg } ->
   workers := List.map (function
     | { cancel } as w when !cancel = false -> w
-    | _ -> let n = !count in incr count; create_worker extra_arg x n)
+    | _ -> let n = !count in incr count; create_worker extra_arg x priority n)
   !workers
 end
 
@@ -102,7 +102,7 @@ end
 
 let is_empty x = locking x begin fun { workers } -> !workers = [] end
 
-let create extra_arg ~size = let x = {
+let create extra_arg ~size priority = let x = {
     lock = Mutex.create ();
     pool = {
       extra_arg;
@@ -110,7 +110,7 @@ let create extra_arg ~size = let x = {
       count = ref size;
   }} in
   locking x begin fun { workers } ->
-     workers := CList.init size (create_worker extra_arg x)
+     workers := CList.init size (create_worker extra_arg x priority)
   end;
   x