1.1 --- a/src/Pure/Concurrent/future.ML	Thu Oct 13 13:49:55 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Oct 13 22:50:35 2011 +0200
     1.3 @@ -552,7 +552,7 @@
     1.4  
     1.5  fun value_result (res: 'a Exn.result) =
     1.6    let
     1.7 -    val task = Task_Queue.dummy_task ();
     1.8 +    val task = Task_Queue.dummy_task;
     1.9      val group = Task_Queue.group_of_task task;
    1.10      val result = Single_Assignment.var "value" : 'a result;
    1.11      val _ = assign_result group result res;

     2.1 --- a/src/Pure/Concurrent/task_queue.ML	Thu Oct 13 13:49:55 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/task_queue.ML	Thu Oct 13 22:50:35 2011 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    val str_of_group: group -> string
     2.5    val str_of_groups: group -> string
     2.6    type task
     2.7 -  val dummy_task: unit -> task
     2.8 +  val dummy_task: task
     2.9    val group_of_task: task -> group
    2.10    val name_of_task: task -> string
    2.11    val pri_of_task: task -> int
    2.12 @@ -102,22 +102,23 @@
    2.13  
    2.14  type timing = Time.time * Time.time * string list;  (*run, wait, wait dependencies*)
    2.15  
    2.16 -fun new_timing () =
    2.17 -  Synchronized.var "timing" ((Time.zeroTime, Time.zeroTime, []): timing);
    2.18 +val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
    2.19 +
    2.20 +fun new_timing () = Synchronized.var "timing" timing_start;
    2.21  
    2.22  abstype task = Task of
    2.23   {group: group,
    2.24    name: string,
    2.25    id: int,
    2.26    pri: int option,
    2.27 -  timing: timing Synchronized.var}
    2.28 +  timing: timing Synchronized.var option}
    2.29  with
    2.30  
    2.31 -fun dummy_task () =
    2.32 -  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = new_timing ()};
    2.33 +val dummy_task =
    2.34 +  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
    2.35  
    2.36  fun new_task group name pri =
    2.37 -  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
    2.38 +  Task {group = group, name = name, id = new_id (), pri = pri, timing = SOME (new_timing ())};
    2.39  
    2.40  fun group_of_task (Task {group, ...}) = group;
    2.41  fun name_of_task (Task {name, ...}) = name;
    2.42 @@ -128,7 +129,8 @@
    2.43  
    2.44  fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
    2.45  
    2.46 -fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
    2.47 +fun timing_of_task (Task {timing, ...}) =
    2.48 +  (case timing of NONE => timing_start | SOME var => Synchronized.value var);
    2.49  
    2.50  fun update_timing update (Task {timing, ...}) e =
    2.51    uninterruptible (fn restore_attributes => fn () =>
    2.52 @@ -136,7 +138,7 @@
    2.53        val start = Time.now ();
    2.54        val result = Exn.capture (restore_attributes e) ();
    2.55        val t = Time.- (Time.now (), start);
    2.56 -      val _ = Synchronized.change timing (update t);
    2.57 +      val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
    2.58      in Exn.release result end) ();
    2.59  
    2.60  fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =