The standard library Weak_Reference api defines access to “weak” references. These are references which are ignored by the garbage collector.
Weak references are useful when, for example, one wants to keep an index of the existing members of a given class of values without preventing them from being garbage-collected when no longer needed.
The Finalize implementation is also built upon the weak pointer facility.
The Weak_Reference api is implemented by the weak_reference package.
The Weak_Reference api source code is in src/lib/std/src/nj/weak-reference.api. The above information is manually maintained and may contain errors.
api {
Weak_Reference X;
make_weak_reference : X -> Weak_Reference(X );
get_normal_reference_from_weak_reference : Weak_Reference(X ) -> Null_Or(X );
Weak_Reference';
make_weak_reference' : X -> Weak_Reference';
get_normal_reference_from_weak_reference' : Weak_Reference' -> Bool;};