diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:11:41 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:16:49 +0100 |
| commit | 20c98eab851210702b39e1c66e005acfc351d8dd (patch) | |
| tree | 957aab7aadfda8c10f251ff9d83f3f5b05c07dc5 /stm/asyncTaskQueue.ml | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
Proper nametab handling of global universe names
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
Diffstat (limited to 'stm/asyncTaskQueue.ml')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4662c5543..cd22a7183 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -58,7 +58,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Univ.Level.t list + | MoreDataUnivLevel of Universes.universe_id list let slave_respond (Request r) = let res = T.perform r in @@ -169,8 +169,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_level (Global.current_dirpath ())) in + CList.init n (fun _ -> Universes.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -309,7 +308,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_level (bufferize (fun () -> + Universes.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)); |