src/Pure/Concurrent/synchronized.ML
changeset 59147 eb3e399f5b9f
parent 59139 e557a9ddee5f
child 59195 f8588372d70e
--- a/src/Pure/Concurrent/synchronized.ML	Thu Dec 18 15:21:54 2014 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Dec 18 16:13:54 2014 +0100
@@ -8,6 +8,7 @@
 sig
   type 'a var
   val var: string -> 'a -> 'a var
+  val peek: 'a var -> 'a
   val value: 'a var -> 'a
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -33,6 +34,8 @@
   cond = ConditionVar.conditionVar (),
   var = Unsynchronized.ref x};
 
+fun peek (Var {var, ...}) = ! var;
+
 fun value (Var {name, lock, var, ...}) =
   Multithreading.synchronized name lock (fn () => ! var);