# HG changeset patch
# User wenzelm
# Date 1519031137 -3600
# Node ID ef20d4961f866fc34e7f7128f12f3f6211db347b
# Parent  8f4810b9d9d1afffa7a532249f1b0ef34fe7f5dd
more operations;

diff -r 8f4810b9d9d1 -r ef20d4961f86 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Mon Feb 19 10:05:37 2018 +0100
@@ -18,6 +18,7 @@
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val force_list: 'a lazy list -> 'a list
+  val forced: 'a lazy -> 'a lazy
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   val future: Future.params -> 'a lazy -> 'a future
 end;
@@ -51,6 +52,8 @@
         Expr _ => true
       | Result _ => false);
 
+fun is_value (Value _) = true
+  | is_value (Lazy _) = false;
 
 
 (* status *)
@@ -109,6 +112,8 @@
   (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
    map force xs);
 
+fun forced x = if is_value x then x else value (force x);
+
 fun map f x = lazy_name "Lazy.map" (fn () => f (force x));