# 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));