Date: Thu, 20 Mar 1997 13:12:16 +0100
From: Emmanuel Engel <Emmanuel.Engel@lri.fr>
Subject: Weak pointers
I wonder when Weaks pointers are erased by the GC. As soon
as it can be or when there is no more memory ? In the second
case, does all the weaks pointers that can be erased are erased
or just enough to allocate new memory. In this case, which are
erased, the older or the younger ?
Is it a good idea to use weak pointers to implement more
or less a cache ?
type ('a,'b) cache = (* In fact a binary tree *)
Node of 'a * 'b * ('a,'b)cache Weak.t
and to use the usual fonctions over binary tree.
- Emmanuel Engel
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:10 MET