src/Pure/PIDE/execution.ML
changeset 56297 3925634718fb
parent 56296 5413b6379c0e
child 56303 4cc3f4db3447
--- 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) =>