force: non-critical, but also non-thread-safe (potentially multiple evaluations);
authorwenzelm
Thu, 16 Aug 2007 21:52:08 +0200
changeset 24299 91d893799212
parent 24298 229fdfc1ddd9
child 24300 e170cee91c66
force: non-critical, but also non-thread-safe (potentially multiple evaluations);
src/Pure/General/susp.ML
--- a/src/Pure/General/susp.ML	Thu Aug 16 21:52:07 2007 +0200
+++ b/src/Pure/General/susp.ML	Thu Aug 16 21:52:08 2007 +0200
@@ -2,7 +2,8 @@
     ID:         $Id$
     Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
 
-Delayed evaluation.
+Delayed evaluation. Supposed to be value oriented; may result in
+multiple evaluations in a multi-threaded environment!
 *)
 
 signature SUSP =
@@ -28,14 +29,14 @@
 
 fun delay f = ref (Delay f);
 
-fun force susp = NAMED_CRITICAL "susp" (fn () =>
+fun force susp =
   (case ! susp of
     Value v => v
   | Delay f =>
       let
         val v = f ();
         val _ = susp := Value v;
-      in v end));
+      in v end);
 
 fun peek susp =
   (case ! susp of
@@ -44,4 +45,4 @@
 
 fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
 
-end
+end;