diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 04:27:21 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-11 12:43:25 +0100 |
commit | 50159f9c1748ccf1d66341d171081a998d116d2f (patch) | |
tree | ef58c58b10abcb45142b56d261bc15f034b2731e /tools | |
parent | a758aac39aa330911f5f589ab3cae1bebed1e9ce (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 'tools')
-rw-r--r-- | tools/coqworkmgr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index e1d1c60d7..f4777c4fb 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -14,7 +14,7 @@ type party = { sock : Unix.file_descr; cout : out_channel; mutable tokens : int; - priority : Flags.priority; + priority : priority; } let answer party msg = @@ -42,10 +42,10 @@ end = struct let is_empty q = !q = [] let rec split acc = function | [] -> List.rev acc, [] - | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | (_, { priority = Low }) :: _ as l -> List.rev acc, l | x :: xs -> split (x :: acc) xs let push (_,{ priority } as item) q = - if priority = Flags.Low then q := !q @ [item] + if priority = Low then q := !q @ [item] else let high, low = split [] !q in q := high @ (item :: low) @@ -148,7 +148,7 @@ let check_alive s = | Some s -> let cout = Unix.out_channel_of_descr s in set_binary_mode_out cout true; - output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request (Hello Low)); flush cout; output_string cout (print_request Ping); flush cout; begin match Unix.select [s] [] [] 1.0 with | [s],_,_ -> |