diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 19:26:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
| commit | a51dda2344679dc6d9145f3f34acad29721f6c75 (patch) | |
| tree | c9ed50095ae459dabd97d9571566647439cf5269 /stm | |
| parent | b0ef649660542ae840ea945d7ab4f1f3ae7b85cd (diff) | |
Split off Universes functions dealing with generating new universes.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index b3e1500ae..38fd817da 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,7 +60,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Universes.universe_id list + | MoreDataUnivLevel of UnivGen.universe_id list let slave_respond (Request r) = let res = T.perform r in @@ -171,7 +171,7 @@ module Make(T : Task) () = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init n (fun _ -> Universes.new_univ_id ()) in + CList.init n (fun _ -> UnivGen.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -310,7 +310,7 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); (* We ask master to allocate universe identifiers *) - Universes.set_remote_new_univ_id (bufferize (fun () -> + UnivGen.set_remote_new_univ_id (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with | MoreDataUnivLevel l -> l)); |