just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

--- a/src/Pure/General/timing.ML	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/General/timing.ML	Tue Apr 09 20:16:52 2013 +0200
@@ -23,7 +23,8 @@
   val is_relevant_time: Time.time -> bool
   val is_relevant: timing -> bool
   val message: timing -> string
-  val status: ('a -> 'b) -> 'a -> 'b
+  val protocol_message: Properties.T -> timing -> unit
+  val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b
 end
 
 structure Timing: TIMING =
@@ -103,10 +104,13 @@
 fun timeap f x = timeit (fn () => f x);
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
-fun status f x =
+fun protocol_message props t =
+  Output.try_protocol_message (props @ Markup.timing_properties t) "";
+
+fun protocol props f x =
   let
     val (t, result) = timing (Exn.interruptible_capture f) x;
-    val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else ();
+    val _ = protocol_message props t;
   in Exn.release result end;
 
 end;

--- a/src/Pure/Isar/proof.ML	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 09 20:16:52 2013 +0200
@@ -1154,16 +1154,20 @@
 end;
 
 
-(* terminal proofs *)
+(* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
 
 local
 
 fun future_terminal_proof proof1 proof2 done int state =
   if Goal.future_enabled_level 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
-      Goal.fork_params
-        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
-        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
+      let
+        val pos = Position.thread_data ();
+        val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
+      in
+        Goal.fork_params {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
+          (fn () => ((), Timing.protocol props proof2 state'))
+      end) |> snd |> done
   else proof1 state;
 
 in

--- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 20:16:52 2013 +0200
@@ -89,7 +89,6 @@
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
-  val approximative_id: transition -> {file: string, offset: int, name: string} option
   val get_timing: transition -> Time.time option
   val put_timing: Time.time option -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
@@ -591,19 +590,6 @@
 fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
 
 
-(* approximative identification within source file *)
-
-fun approximative_id tr =
-  let
-    val name = name_of tr;
-    val pos = pos_of tr;
-  in
-    (case (Position.file_of pos, Position.offset_of pos) of
-      (SOME file, SOME offset) => SOME {file = file, offset = offset, name = name}
-    | _ => NONE)
-  end;
-
-
 (* thread position *)
 
 fun setmp_thread_position (Transition {pos, ...}) f x =
@@ -643,23 +629,9 @@
       val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
 
       val timing_result = Timing.result timing_start;
-
-      val _ =
-        if Timing.is_relevant timing_result andalso (! profiling > 0 orelse ! timing)
-          andalso not (Keyword.is_control (name_of tr))
-        then tracing (command_msg "" tr ^ ": " ^ Timing.message timing_result)
-        else ();
-      val _ =
-        if Timing.is_relevant timing_result
-        then status tr (Markup.timing timing_result)
-        else ();
-      val _ =
-        (case approximative_id tr of
-          SOME id =>
-            (Output.try_protocol_message
-              (Markup.command_timing ::
-                Markup.command_timing_properties id (#elapsed timing_result)) "")
-        | NONE => ());
+      val timing_props =
+        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
+      val _ = Timing.protocol_message timing_props timing_result;
     in
       (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
     end);

--- a/src/Pure/PIDE/markup.scala	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Apr 09 20:16:52 2013 +0200
@@ -193,6 +193,7 @@
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
+
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
@@ -206,6 +207,7 @@
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
+
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
@@ -214,6 +216,22 @@
   }
 
 
+  /* command timing */
+
+  object Command_Timing
+  {
+    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+      props match {
+        case (FUNCTION, "command_timing") :: args =>
+          (args, args) match {
+            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
+
   /* toplevel */
 
   val SUBGOALS = "subgoals"

--- a/src/Pure/System/isar.ML	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/System/isar.ML	Tue Apr 09 20:16:52 2013 +0200
@@ -118,6 +118,23 @@
 
 local
 
+fun protocol_message props output =
+  (case props of
+    function :: args =>
+      if function = Markup.command_timing then
+        let
+          val name = the_default "" (Properties.get args Markup.nameN);
+          val pos = Position.of_properties args;
+          val timing = Markup.parse_timing_properties args;
+        in
+          if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
+            andalso name <> "" andalso not (Keyword.is_control name)
+          then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
+          else ()
+        end
+      else raise Output.Protocol_Message props
+  | [] => raise Output.Protocol_Message props);
+
 fun raw_loop secure src =
   let
     fun check_secure () =
@@ -139,6 +156,7 @@
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
   if do_init then (Options.load_default (); init ()) else ();
+  Output.Private_Hooks.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 

--- a/src/Pure/System/session.scala	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/System/session.scala	Tue Apr 09 20:16:52 2013 +0200
@@ -300,22 +300,31 @@
     def handle_output(output: Isabelle_Process.Output)
     //{{{
     {
-      def bad_output(output: Isabelle_Process.Output)
+      def bad_output()
       {
         if (verbose)
           System.err.println("Ignoring prover output: " + output.message.toString)
       }
 
+      def accumulate(state_id: Document.ID, message: XML.Elem)
+      {
+        try {
+          val st = global_state >>> (_.accumulate(state_id, message))
+          delay_commands_changed.invoke(false, List(st.command))
+        }
+        catch {
+          case _: Document.State.Fail => bad_output()
+        }
+      }
+
       output.properties match {
 
         case Position.Id(state_id) if !output.is_protocol =>
-          try {
-            val st = global_state >>> (_.accumulate(state_id, output.message))
-            delay_commands_changed.invoke(false, List(st.command))
-          }
-          catch {
-            case _: Document.State.Fail => bad_output(output)
-          }
+          accumulate(state_id, output.message)
+
+        case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
+          // FIXME XML.cache (!?)
+          accumulate(state_id, XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))))
 
         case Markup.Assign_Execs if output.is_protocol =>
           XML.content(output.body) match {
@@ -324,8 +333,8 @@
                 val cmds = global_state >>> (_.assign(id, assign))
                 delay_commands_changed.invoke(true, cmds)
               }
-              catch { case _: Document.State.Fail => bad_output(output) }
-            case _ => bad_output(output)
+              catch { case _: Document.State.Fail => bad_output() }
+            case _ => bad_output()
           }
           // FIXME separate timeout event/message!?
           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
@@ -340,8 +349,8 @@
               try {
                 global_state >> (_.removed_versions(removed))
               }
-              catch { case _: Document.State.Fail => bad_output(output) }
-            case _ => bad_output(output)
+              catch { case _: Document.State.Fail => bad_output() }
+            case _ => bad_output()
           }
 
         case Markup.Invoke_Scala(name, id) if output.is_protocol =>
@@ -374,7 +383,7 @@
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
 
-        case _ => bad_output(output)
+        case _ => bad_output()
       }
     }
     //}}}

--- a/src/Pure/Tools/build.ML	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/Tools/build.ML	Tue Apr 09 20:16:52 2013 +0200
@@ -12,16 +12,56 @@
 structure Build: BUILD =
 struct
 
+(* command timings *)
+
+type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
+
+val empty_timings: timings = Symtab.empty;
+
+fun update_timings props =
+  (case Markup.parse_command_timing_properties props of
+    SOME ({file, offset, name}, time) =>
+      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
+  | NONE => I);
+
+fun approximative_id name pos =
+  (case (Position.file_of pos, Position.offset_of pos) of
+    (SOME file, SOME offset) =>
+      if name = "" then NONE else SOME {file = file, offset = offset, name = name}
+  | _ => NONE);
+
+fun lookup_timings timings tr =
+  (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
+    SOME {file, offset, name} =>
+      (case Symtab.lookup timings file of
+        SOME offsets =>
+          (case Inttab.lookup offsets offset of
+            SOME (name', time) => if name = name' then SOME time else NONE
+          | NONE => NONE)
+      | NONE => NONE)
+  | NONE => NONE);
+
+
 (* protocol messages *)
 
-(* FIXME avoid hardwired stuff!? *)
-val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
+fun inline_message a args =
+  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
 
 fun protocol_message props output =
   (case props of
     function :: args =>
-      if member (op =) protocol_echo function then
-        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
+      if function = Markup.ML_statistics orelse function = Markup.task_statistics then
+        inline_message (#2 function) args
+      else if function = Markup.command_timing then
+        let
+          val name = the_default "" (Properties.get args Markup.nameN);
+          val pos = Position.of_properties args;
+          val {elapsed, ...} = Markup.parse_timing_properties args;
+        in
+          (case approximative_id name pos of
+            SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
+          | NONE => ())
+        end
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
@@ -74,30 +114,6 @@
           " (undefined " ^ commas conds ^ ")\n"))
   end;
 
-
-(* command timings *)
-
-type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
-
-val empty_timings: timings = Symtab.empty;
-
-fun update_timings props =
-  (case Markup.parse_command_timing_properties props of
-    SOME ({file, offset, name}, time) =>
-      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
-  | NONE => I);
-
-fun lookup_timings timings tr =
-  (case Toplevel.approximative_id tr of
-    SOME {file, offset, name} =>
-      (case Symtab.lookup timings file of
-        SOME offsets =>
-          (case Inttab.lookup offsets offset of
-            SOME (name', time) => if name = name' then SOME time else NONE
-          | NONE => NONE)
-      | NONE => NONE)
-  | NONE => NONE);
-
 in
 
 fun build args_file = Command_Line.tool (fn () =>