peek value without synchronization;
authorwenzelm
Thu, 18 Dec 2014 16:13:54 +0100
changeset 59147 eb3e399f5b9f
parent 59146 ba2a326fc271
child 59148 7a373a35a37a
peek value without synchronization;
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/synchronized.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);
 
--- 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);