back to full synchronization (cf. eb3e399f5b9f);
authorwenzelm
Sun, 28 Dec 2014 22:10:09 +0100
changeset 59195 f8588372d70e
parent 59194 b51489b75bb9
child 59196 73a6403637b3
back to full synchronization (cf. eb3e399f5b9f);
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/synchronized_sequential.ML
--- 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 =