--- a/src/Pure/Concurrent/unsynchronized.ML Wed May 10 15:43:49 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Wed May 10 16:05:14 2023 +0200
@@ -18,6 +18,7 @@
type 'a weak_ref = 'a ref option ref
val weak_ref: 'a -> 'a weak_ref
val weak_peek: 'a weak_ref -> 'a option
+ val weak_active: 'a weak_ref -> bool
end;
structure Unsynchronized: UNSYNCHRONIZED =
@@ -58,6 +59,9 @@
fun weak_peek (ref (SOME (ref a))) = SOME a
| weak_peek _ = NONE;
+fun weak_active (ref (SOME (ref _))) = true
+ | weak_active _ = false;
+
end;
ML_Name_Space.forget_val "ref";