aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
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 /tools
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 'tools')
-rw-r--r--tools/coqworkmgr.ml8
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],_,_ ->