added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
misc tuning;

--- a/src/Pure/PIDE/command.ML	Wed Mar 26 09:19:04 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Mar 26 12:15:42 2014 +0100
@@ -20,7 +20,7 @@
     eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print_function =
-    {command_name: string, args: string list} ->
+    {command_name: string, args: string list, exec_id: Document_ID.exec} ->
       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
   val print_function: string -> print_function -> unit
   val no_print_function: string -> unit
@@ -172,9 +172,10 @@
 
 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
 
-fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
+fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
+val eval_eq = op = o pairself eval_exec_id;
 
-fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id;
+val eval_running = Execution.is_running_exec o eval_exec_id;
 fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
 
 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
@@ -260,10 +261,13 @@
  {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit memo};
 
+fun print_exec_id (Print {exec_id, ...}) = exec_id;
+val print_eq = op = o pairself print_exec_id;
+
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
-  {command_name: string, args: string list} ->
+  {command_name: string, args: string list, exec_id: Document_ID.exec} ->
     {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
 
 local
@@ -277,8 +281,6 @@
       if Exn.is_interrupt exn then reraise exn
       else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
 
-fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
-
 fun print_finished (Print {print_process, ...}) = memo_finished print_process;
 
 fun print_persistent (Print {persistent, ...}) = persistent;
@@ -315,7 +317,7 @@
 
     fun new_print name args get_pr =
       let
-        val params = {command_name = command_name, args = args};
+        val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
       in
         (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
@@ -353,6 +355,14 @@
 end;
 
 val _ =
+  print_function "Execution.print"
+    (fn {args, exec_id, ...} =>
+      if null args then
+        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+          print_fn = fn _ => fn _ => Execution.apply_prints exec_id}
+      else NONE);
+
+val _ =
   print_function "print_state"
     (fn {command_name, ...} =>
       SOME {delay = NONE, pri = 1, persistent = false, strict = true,
@@ -373,8 +383,7 @@
   (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
 
 fun exec_ids NONE = []
-  | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
-      exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
+  | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
 
 local
 

--- a/src/Pure/PIDE/execution.ML	Wed Mar 26 09:19:04 2014 +0100
+++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 12:15:42 2014 +0100
@@ -16,6 +16,8 @@
   val cancel: Document_ID.exec -> unit
   val terminate: Document_ID.exec -> unit
   val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
+  val print: (serial -> unit) -> unit
+  val apply_prints: Document_ID.exec -> unit
   val purge: Document_ID.exec list -> unit
   val reset: unit -> Future.group list
   val shutdown: unit -> unit
@@ -26,18 +28,19 @@
 
 (* global state *)
 
-datatype state = State of
-  {execution: Document_ID.execution,  (*overall document execution*)
-   execs: Future.group list Inttab.table};  (*command execs with registered forks*)
+type exec_state = Future.group list * (unit -> unit) list;  (*active forks, prints*)
+type state =
+  Document_ID.execution * (*overall document execution*)
+  exec_state Inttab.table;  (*running command execs*)
 
-fun make_state (execution, execs) = State {execution = execution, execs = execs};
-fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
-
-val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
+val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
 val state = Synchronized.var "Execution.state" init_state;
 
-fun get_state () = let val State args = Synchronized.value state in args end;
-fun change_state f = Synchronized.change state (map_state f);
+fun get_state () = Synchronized.value state;
+fun change_state_result f = Synchronized.change_result state f;
+fun change_state f = Synchronized.change state f;
+
+fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
 
 
 (* unique running execution *)
@@ -50,29 +53,30 @@
 
 fun discontinue () = change_state (apfst (K Document_ID.none));
 
-fun is_running execution_id = execution_id = #execution (get_state ());
+fun is_running execution_id = execution_id = #1 (get_state ());
 
 
 (* execs *)
 
 fun is_running_exec exec_id =
-  Inttab.defined (#execs (get_state ())) exec_id;
+  Inttab.defined (#2 (get_state ())) exec_id;
 
 fun running execution_id exec_id groups =
-  Synchronized.change_result state
-    (fn State {execution = execution_id', execs} =>
-      let
-        val continue = execution_id = execution_id';
-        val execs' =
-          if continue then
-            Inttab.update_new (exec_id, groups) execs
-              handle Inttab.DUP dup =>
-                raise Fail ("Execution already registered: " ^ Document_ID.print dup)
-          else execs;
-      in (continue, make_state (execution_id', execs')) end);
+  change_state_result (fn (execution_id', execs) =>
+    let
+      val continue = execution_id = execution_id';
+      val execs' =
+        if continue then
+          Inttab.update_new (exec_id, (groups, [])) execs
+            handle Inttab.DUP dup =>
+              raise Fail ("Execution already registered: " ^ Document_ID.print dup)
+        else execs;
+    in (continue, (execution_id', execs')) end);
 
 fun peek exec_id =
-  Inttab.lookup_list (#execs (get_state ())) exec_id;
+  (case Inttab.lookup (#2 (get_state ())) exec_id of
+    SOME (groups, _) => groups
+  | NONE => []);
 
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
 fun terminate exec_id = List.app Future.terminate (peek exec_id);
@@ -90,9 +94,10 @@
       val exec_id = the_default 0 (Position.parse_id pos);
       val group = Future.worker_subgroup ();
       val _ = change_state (apsnd (fn execs =>
-        if Inttab.defined execs exec_id
-        then Inttab.cons_list (exec_id, group) execs
-        else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
+        (case Inttab.lookup execs exec_id of
+          SOME (groups, prints) =>
+            Inttab.update (exec_id, (group :: groups, prints)) execs
+        | NONE => raise Fail (unregistered exec_id))));
 
       val future =
         (singleton o Future.forks)
@@ -121,6 +126,37 @@
     in future end)) ();
 
 
+(* print *)
+
+fun print pr =
+  change_state (apsnd (fn execs =>
+    let
+      val exec_id = the_default 0 (Position.parse_id (Position.thread_data ()));
+      val i = serial ();
+    in
+      (case Inttab.lookup execs exec_id of
+        SOME (groups, prints) =>
+          Inttab.update (exec_id, (groups, (fn () => pr i) :: prints)) execs
+      | NONE => raise Fail (unregistered exec_id))
+    end));
+
+fun apply_prints exec_id =
+  (case Inttab.lookup (#2 (get_state ())) exec_id of
+    SOME (_, prints) =>
+      if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
+      then List.app (fn e => e ()) (rev prints)
+      else
+        let
+          val pos = Position.thread_data ();
+          val pri =
+            (case Future.worker_task () of
+              SOME task => Task_Queue.pri_of_task task
+            | NONE => 0);
+          val futures = map (fork {name = "Execution.print", pos = pos, pri = pri}) (rev prints);
+        in ignore (Future.joins futures) end
+  | NONE => raise Fail (unregistered exec_id));
+
+
 (* cleanup *)
 
 fun purge exec_ids =
@@ -128,7 +164,7 @@
     let
       val execs' = fold Inttab.delete_safe exec_ids execs;
       val () =
-        (execs', ()) |-> Inttab.fold (fn (exec_id, groups) => fn () =>
+        (execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () =>
           if Inttab.defined execs' exec_id then ()
           else groups |> List.app (fn group =>
             if Task_Queue.is_canceled group then ()
@@ -136,8 +172,8 @@
     in execs' end);
 
 fun reset () =
-  Synchronized.change_result state (fn State {execs, ...} =>
-    let val groups = Inttab.fold (append o #2) execs []
+  change_state_result (fn (_, execs) =>
+    let val groups = Inttab.fold (append o #1 o #2) execs []
     in (groups, init_state) end);
 
 fun shutdown () =