added constant value;

--- 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 **)