change API for local FLS hmap

This commit is contained in:
Simon Cruanes 2024-08-29 16:07:27 -04:00
parent 44e335e0b0
commit 328ecf4ea5
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4

View file

@ -23,15 +23,15 @@ let[@inline] update_local_hmap (f : Hmap.t -> Hmap.t) : unit =
FLS.set fiber k_local_hmap h FLS.set fiber k_local_hmap h
(** @raise Invalid_argument if not present *) (** @raise Invalid_argument if not present *)
let get_exn (k : 'a Hmap.key) : 'a = let get_in_local_hmap_exn (k : 'a Hmap.key) : 'a =
let h = get_local_hmap () in let h = get_local_hmap () in
Hmap.get k h Hmap.get k h
let get_opt (k : 'a Hmap.key) : 'a option = let get_in_local_hmap_opt (k : 'a Hmap.key) : 'a option =
let h = get_local_hmap () in let h = get_local_hmap () in
Hmap.find k h Hmap.find k h
let[@inline] set (k : 'a Hmap.key) (v : 'a) : unit = let[@inline] set_in_local_hmap (k : 'a Hmap.key) (v : 'a) : unit =
update_local_hmap (Hmap.add k v) update_local_hmap (Hmap.add k v)
(**/**) (**/**)