# HG changeset patch
# User wenzelm
# Date 1248786318 -7200
# Node ID fd5e4a1a4ea6d7ff65c14db49cd310803a2e4834
# Parent  e586c82fdf69802e66effd92777c00cdb79cde61
added unsynchronized Synchronized.peek;

diff -r e586c82fdf69 -r fd5e4a1a4ea6 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue Jul 28 14:54:53 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue Jul 28 15:05:18 2009 +0200
@@ -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
@@ -32,6 +33,8 @@
   cond = ConditionVar.conditionVar (),
   var = ref x};
 
+fun peek (Var {var, ...}) = ! var;  (*unsynchronized!*)
+
 fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);