optional timing, to avoid redundant allocation of mutable cells;

--- a/src/Pure/Concurrent/task_queue.ML	Sat Nov 05 22:41:25 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Sun Nov 06 13:25:41 2011 +0100
@@ -104,7 +104,9 @@
 
 val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
 
-fun new_timing () = Synchronized.var "timing" timing_start;
+fun new_timing () =
+  if ! Multithreading.trace < 2 then NONE
+  else SOME (Synchronized.var "timing" timing_start);
 
 abstype task = Task of
  {group: group,
@@ -118,7 +120,7 @@
   Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
 
 fun new_task group name pri =
-  Task {group = group, name = name, id = new_id (), pri = pri, timing = SOME (new_timing ())};
+  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
 
 fun group_of_task (Task {group, ...}) = group;
 fun name_of_task (Task {name, ...}) = name;