# HG changeset patch
# User wenzelm
# Date 1683642668 -7200
# Node ID e5c146904c90e61139da6379dac42a8bf6fdbe80
# Parent  f589c50e54a0096fa4852c9bdab32c602611fb70
clarified signature;

diff -r f589c50e54a0 -r e5c146904c90 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue May 09 09:49:41 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue May 09 16:31:08 2023 +0200
@@ -107,11 +107,11 @@
 
 fun cache_eval (Cache {expr, var}) =
   change_result var (fn state =>
-    (case state of
-      SOME (Unsynchronized.ref (SOME (Unsynchronized.ref result))) => (result, state)
-    | _ =>
-      let val result = expr ()
-      in (result, SOME (Unsynchronized.weak_ref result)) end));
+    (case Option.mapPartial Unsynchronized.weak_peek state of
+      SOME result => (result, state)
+    | NONE =>
+        let val result = expr ()
+        in (result, SOME (Unsynchronized.weak_ref result)) end));
 
 end;
 
diff -r f589c50e54a0 -r e5c146904c90 src/Pure/Concurrent/unsynchronized.ML
--- a/src/Pure/Concurrent/unsynchronized.ML	Tue May 09 09:49:41 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Tue May 09 16:31:08 2023 +0200
@@ -17,11 +17,14 @@
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   type 'a weak_ref = 'a ref option ref
   val weak_ref: 'a -> 'a weak_ref
+  val weak_peek: 'a weak_ref -> 'a option
 end;
 
 structure Unsynchronized: UNSYNCHRONIZED =
 struct
 
+(* regular references *)
+
 datatype ref = datatype ref;
 
 val op := = op :=;
@@ -43,9 +46,16 @@
       val _ = flag := orig_value;
     in Exn.release result end) ();
 
+
+(* weak references *)
+
 type 'a weak_ref = 'a ref option ref;
+
 fun weak_ref a = Weak.weak (SOME (ref a));
 
+fun weak_peek (ref (SOME (ref a))) = SOME a
+  | weak_peek _ = NONE;
+
 end;
 
 ML_Name_Space.forget_val "ref";
diff -r f589c50e54a0 -r e5c146904c90 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue May 09 09:49:41 2023 +0200
+++ b/src/Pure/context.ML	Tue May 09 16:31:08 2023 +0200
@@ -223,10 +223,10 @@
     val trace1 = Synchronized.value theory_tokens;
     val trace2 = Synchronized.value proof_tokens;
 
-    fun cons1 (Unsynchronized.ref (SOME (Unsynchronized.ref (thy as Thy _)))) = cons (Theory thy)
-      | cons1 _ = I;
-    fun cons2 (Unsynchronized.ref (SOME (Unsynchronized.ref (ctxt as Prf _)))) = cons (Proof ctxt)
-      | cons2 _ = I;
+    fun cons1 r =
+      (case Unsynchronized.weak_peek r of SOME (thy as Thy _) => cons (Theory thy) | _ => I);
+    fun cons2 r =
+      (case Unsynchronized.weak_peek r of SOME (ctxt as Prf _) => cons (Proof ctxt) | _ => I);
 
     val contexts = build (fold cons1 trace1 #> fold cons2 trace2);
     val active_theories = fold (fn Theory _ => Integer.add 1 | _ => I) contexts 0;