# HG changeset patch
# User wenzelm
# Date 1683657169 -7200
# Node ID 620d0a5d61a2e9e6516fcfbda4d04bb740ba9d66
# Parent  91fc15d9dbdf6c11a8ad55e62098b6b21d31d261
more operations;

diff -r 91fc15d9dbdf -r 620d0a5d61a2 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue May 09 19:56:31 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue May 09 20:32:49 2023 +0200
@@ -16,6 +16,7 @@
   val change: 'a var -> ('a -> 'a) -> unit
   type 'a cache
   val cache: (unit -> 'a) -> 'a cache
+  val cache_peek: 'a cache -> 'a option
   val cache_eval: 'a cache -> 'a
 end;
 
@@ -105,6 +106,9 @@
 fun cache expr =
   Cache {expr = expr, var = var "Synchronized.cache" NONE};
 
+fun cache_peek (Cache {var, ...}) =
+  Option.mapPartial Unsynchronized.weak_peek (value var);
+
 fun cache_eval (Cache {expr, var}) =
   change_result var (fn state =>
     (case Option.mapPartial Unsynchronized.weak_peek state of