# HG changeset patch # User wenzelm # Date 1419801009 -3600 # Node ID f8588372d70e4cdcadf7280cef3160dd8a5e7000 # Parent b51489b75bb95615f98c0745baaffac06e942680 back to full synchronization (cf. eb3e399f5b9f); diff -r b51489b75bb9 -r f8588372d70e src/Pure/Concurrent/lazy.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); diff -r b51489b75bb9 -r f8588372d70e src/Pure/Concurrent/synchronized.ML --- 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); diff -r b51489b75bb9 -r f8588372d70e src/Pure/Concurrent/synchronized_sequential.ML --- 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 =