# HG changeset patch
# User wenzelm
# Date 1228518117 -3600
# Node ID 1b99dcae2156b525bd927d3e11f19552b0e4bd45
# Parent  01918abaa9e7690900167826552b1eb7daaaa44d
added constant value;

diff -r 01918abaa9e7 -r 1b99dcae2156 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Concurrent/future.ML	Sat Dec 06 00:01:57 2008 +0100
@@ -36,6 +36,7 @@
   val group_of: 'a future -> group
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
+  val value: 'a -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val fork_group: group -> (unit -> 'a) -> 'a future
   val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
@@ -84,6 +85,11 @@
 fun peek (Future {result, ...}) = ! result;
 fun is_finished x = is_some (peek x);
 
+fun value x = Future
+ {task = TaskQueue.new_task (),
+  group = TaskQueue.new_group (),
+  result = ref (SOME (Exn.Result x))};
+
 
 
 (** scheduling **)