more systematic task statistics;

--- a/src/Pure/Concurrent/future.ML	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Jan 18 17:51:50 2013 +0100
@@ -256,12 +256,11 @@
       Task_Queue.running task (fn () =>
         setmp_worker_task task (fn () =>
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
-    val _ = Multithreading.tracing 2 (fn () =>
-      let
-        val s = Task_Queue.str_of_task_groups task;
-        fun micros time = string_of_int (Time.toNanoseconds time div 1000);
-        val (run, wait, deps) = Task_Queue.timing_of_task task;
-      in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
+    val _ =
+      if ! Multithreading.trace >= 2 then
+        Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
+          handle Fail msg => warning msg
+      else ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);

--- a/src/Pure/Concurrent/task_queue.ML	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Jan 18 17:51:50 2013 +0100
@@ -22,7 +22,7 @@
   val pri_of_task: task -> int
   val str_of_task: task -> string
   val str_of_task_groups: task -> string
-  val timing_of_task: task -> Time.time * Time.time * string list
+  val task_statistics: task -> Properties.T
   val running: task -> (unit -> 'a) -> 'a
   val joining: task -> (unit -> 'a) -> 'a
   val waiting: task -> task list -> (unit -> 'a) -> 'a
@@ -114,14 +114,17 @@
   name: string,
   id: int,
   pri: int option,
-  timing: timing Synchronized.var option}
+  timing: timing Synchronized.var option,
+  pos: Position.T}
 with
 
 val dummy_task =
-  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
+  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
+    pos = Position.none};
 
 fun new_task group name pri =
-  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
+  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
+    pos = Position.thread_data ()};
 
 fun group_of_task (Task {group, ...}) = group;
 fun name_of_task (Task {name, ...}) = name;
@@ -132,9 +135,6 @@
 
 fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
 
-fun timing_of_task (Task {timing, ...}) =
-  (case timing of NONE => timing_start | SOME var => Synchronized.value var);
-
 fun update_timing update (Task {timing, ...}) e =
   uninterruptible (fn restore_attributes => fn () =>
     let
@@ -147,6 +147,18 @@
 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
   prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
 
+fun task_statistics (Task {name, id, timing, pos, ...}) =
+  let
+    val (run, wait, wait_deps) =
+      (case timing of NONE => timing_start | SOME var => Synchronized.value var);
+    fun micros time = string_of_int (Time.toNanoseconds time div 1000);
+  in
+    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+     ("task_name", name), ("task_id", Markup.print_int id),
+     ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
+    Position.properties_of pos
+  end;
+
 end;
 
 structure Tasks = Table(type key = task val ord = task_ord);

--- a/src/Pure/PIDE/markup.ML	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Jan 18 17:51:50 2013 +0100
@@ -134,6 +134,7 @@
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
+  val task_statistics: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val no_output: Output.output * Output.output
@@ -412,6 +413,8 @@
 
 val ML_statistics = (functionN, "ML_statistics");
 
+val task_statistics = (functionN, "task_statistics");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name

--- a/src/Pure/PIDE/markup.scala	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 18 17:51:50 2013 +0100
@@ -330,6 +330,15 @@
         case _ => None
       }
   }
+
+  object Task_Statistics
+  {
+    def unapply(props: Properties.T): Option[Properties.T] =
+      props match {
+        case (FUNCTION, "task_statistics") :: stats => Some(stats)
+        case _ => None
+      }
+  }
 }
 
 

--- a/src/Pure/System/session.scala	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/System/session.scala	Fri Jan 18 17:51:50 2013 +0100
@@ -364,6 +364,9 @@
         case Markup.ML_Statistics(props) if output.is_protocol =>
           statistics.event(Session.Statistics(props))
 
+        case Markup.Task_Statistics(props) if output.is_protocol =>
+          // FIXME
+
         case _ if output.is_init =>
           phase = Session.Ready
 

--- a/src/Pure/Tools/build.ML	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/Tools/build.ML	Fri Jan 18 17:51:50 2013 +0100
@@ -19,13 +19,21 @@
       else NONE
   | ML_statistics _ _ = NONE;
 
+fun task_statistics (function :: stats) "" =
+      if function = Markup.task_statistics then SOME stats
+      else NONE
+  | task_statistics _ _ = NONE;
+
 fun protocol_message props output =
   (case ML_statistics props output of
     SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
   | NONE =>
-      (case Markup.dest_loading_theory props of
-        SOME name => writeln ("\floading_theory = " ^ name)
-      | NONE => raise Fail "Undefined Output.protocol_message"));
+      (case task_statistics props output of
+        SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
+      | NONE =>
+          (case Markup.dest_loading_theory props of
+            SOME name => writeln ("\floading_theory = " ^ name)
+          | NONE => raise Fail "Undefined Output.protocol_message")));
 
 
 (* build *)

--- a/src/Pure/Tools/build.scala	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/Tools/build.scala	Fri Jan 18 17:51:50 2013 +0100
@@ -561,14 +561,16 @@
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
 
-  sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
+  sealed case class Log_Info(
+    stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
 
   def parse_log(text: String): Log_Info =
   {
     val lines = split_lines(text)
     val stats = Props.parse_lines("\fML_statistics = ", lines)
+    val tasks = Props.parse_lines("\ftask_statistics = ", lines)
     val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
-    Log_Info(stats, timing)
+    Log_Info(stats, tasks, timing)
   }