# HG changeset patch
# User wenzelm
# Date 1222804965 -7200
# Node ID 29b2886114fb3dc9fc2df8002bcc168561b097d5
# Parent  3d5fbf964a7ee7d13d97246f2dd51c70f6a9c1cd
renamed Future.fork_irrelevant to Future.fork_background;
tuned;

diff -r 3d5fbf964a7e -r 29b2886114fb src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Sep 30 22:02:44 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Sep 30 22:02:45 2008 +0200
@@ -37,7 +37,7 @@
   val is_finished: 'a T -> bool
   val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
   val fork: (unit -> 'a) -> 'a T
-  val fork_irrelevant: (unit -> 'a) -> 'a T
+  val fork_background: (unit -> 'a) -> 'a T
   val join_results: 'a T list -> 'a Exn.result list
   val join: 'a T -> 'a
   val release_results: 'a Exn.result list -> 'a list
@@ -243,8 +243,10 @@
       change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
   in Future {task = task, group = group, result = result} end;
 
-fun fork e = future (Option.map #3 (thread_data ())) [] true e;
-fun fork_irrelevant e = future (Option.map #3 (thread_data ())) [] false e;
+fun fork_common pri = future (Option.map #3 (thread_data ())) [] pri;
+
+fun fork e = fork_common true e;
+fun fork_background e = fork_common false e;
 
 
 (* join: retrieve results *)