# HG changeset patch
# User wenzelm
# Date 1395862335 -3600
# Node ID 3925634718fb335284091dec75f9fb13302a5f58
# Parent  5413b6379c0e74b0621caa48f90973afb1395e34
support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);

diff -r 5413b6379c0e -r 3925634718fb src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Wed Mar 26 20:08:07 2014 +0100
+++ b/src/Pure/General/output.ML	Wed Mar 26 20:32:15 2014 +0100
@@ -30,6 +30,8 @@
   val error_message: string -> unit
   val prompt: string -> unit
   val status: string -> unit
+  val direct_report: string -> unit
+  val redirect_report: (string -> unit) -> ('a -> 'b) -> 'a -> 'b
   val report: string -> unit
   val result: Properties.T -> string -> unit
   val protocol_message: Properties.T -> string -> unit
@@ -115,7 +117,17 @@
 fun error_message s = error_message' (serial (), s);
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn (output s);
-fun report s = ! report_fn (output s);
+
+fun direct_report s = ! report_fn (output s);
+
+local
+  val tag = Universal.tag () : (string -> unit) Universal.tag;
+  fun thread_data () = the_default direct_report (Thread.getLocal tag);
+in
+  fun redirect_report rep = Library.setmp_thread_data tag (thread_data ()) rep;
+  fun report s = thread_data () s;
+end;
+
 fun result props s = ! result_fn props (output s);
 fun protocol_message props s = ! protocol_message_fn props (output s);
 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
diff -r 5413b6379c0e -r 3925634718fb src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Wed Mar 26 20:08:07 2014 +0100
+++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 20:32:15 2014 +0100
@@ -18,6 +18,7 @@
   type params = {name: string, pos: Position.T, pri: int}
   val fork: params -> (unit -> 'a) -> 'a future
   val print: params -> (serial -> unit) -> unit
+  val print_report: string -> unit
   val fork_prints: Document_ID.exec -> unit
   val purge: Document_ID.exec list -> unit
   val reset: unit -> Future.group list
@@ -147,6 +148,14 @@
       | NONE => raise Fail (unregistered exec_id))
     end));
 
+fun print_report s =
+  if s = "" orelse not (Multithreading.enabled ()) then Output.direct_report s
+  else
+    let
+      val body = YXML.parse_body s  (*sharable closure!*)
+      val params = {name = "", pos = Position.thread_data (), pri = 0};
+    in print params (fn _ => Output.direct_report (YXML.string_of_body body)) end;
+
 fun fork_prints exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of
     SOME (_, prints) =>