more operations;

--- 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