back to full synchronization (cf. eb3e399f5b9f);
--- a/src/Pure/Concurrent/lazy.ML Sun Dec 28 22:03:11 2014 +0100
+++ b/src/Pure/Concurrent/lazy.ML Sun Dec 28 22:10:09 2014 +0100
@@ -37,7 +37,7 @@
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
fun peek (Lazy var) =
- (case Synchronized.peek var of
+ (case Synchronized.value var of
Expr _ => NONE
| Result res => Future.peek res);
--- a/src/Pure/Concurrent/synchronized.ML Sun Dec 28 22:03:11 2014 +0100
+++ b/src/Pure/Concurrent/synchronized.ML Sun Dec 28 22:10:09 2014 +0100
@@ -8,7 +8,6 @@
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
@@ -34,8 +33,6 @@
cond = ConditionVar.conditionVar (),
var = Unsynchronized.ref x};
-fun peek (Var {var, ...}) = ! var;
-
fun value (Var {name, lock, var, ...}) =
Multithreading.synchronized name lock (fn () => ! var);
--- a/src/Pure/Concurrent/synchronized_sequential.ML Sun Dec 28 22:03:11 2014 +0100
+++ b/src/Pure/Concurrent/synchronized_sequential.ML Sun Dec 28 22:10:09 2014 +0100
@@ -11,7 +11,6 @@
with
fun var _ x = Var (Unsynchronized.ref x);
-fun peek (Var var) = ! var;
fun value (Var var) = ! var;
fun timed_access (Var var) _ f =