diff --git a/src/util/rpool.mli b/src/util/rpool.mli new file mode 100644 index 0000000..5998658 --- /dev/null +++ b/src/util/rpool.mli @@ -0,0 +1,10 @@ +(** A resource pool (for buffers) *) + +type 'a t + +val create : + max_size:int -> create:(unit -> 'a) -> clear:('a -> unit) -> unit -> 'a t + +val alloc : 'a t -> 'a +val recycle : 'a t -> 'a -> unit +val with_ : 'a t -> ('a -> 'b) -> 'b