# HG changeset patch
# User wenzelm
# Date 1418915634 -3600
# Node ID eb3e399f5b9f878ab38716829ede103c097c633c
# Parent  ba2a326fc271ad778eafd4a1cf730933f28c0445
peek value without synchronization;

diff -r ba2a326fc271 -r eb3e399f5b9f src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Dec 18 15:21:54 2014 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Thu Dec 18 16:13:54 2014 +0100
@@ -32,7 +32,7 @@
 with
 
 fun peek (Lazy var) =
-  (case Synchronized.value var of
+  (case Synchronized.peek var of
     Expr _ => NONE
   | Result res => Future.peek res);
 
diff -r ba2a326fc271 -r eb3e399f5b9f src/Pure/Concurrent/synchronized.ML
--- 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);