# HG changeset patch
# User wenzelm
# Date 1683727514 -7200
# Node ID 82b09fd28504157207c450dc6465f1dbb79cbad1
# Parent  dfa44d85d751606e6394343cd11bb012c283ebd6
more operations;

diff -r dfa44d85d751 -r 82b09fd28504 src/Pure/Concurrent/unsynchronized.ML
--- 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";