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