src/Pure/PIDE/execution.ML
changeset 56297 3925634718fb
parent 56296 5413b6379c0e
child 56303 4cc3f4db3447
     1.1 --- a/src/Pure/PIDE/execution.ML	Wed Mar 26 20:08:07 2014 +0100
     1.2 +++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 20:32:15 2014 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    type params = {name: string, pos: Position.T, pri: int}
     1.5    val fork: params -> (unit -> 'a) -> 'a future
     1.6    val print: params -> (serial -> unit) -> unit
     1.7 +  val print_report: string -> unit
     1.8    val fork_prints: Document_ID.exec -> unit
     1.9    val purge: Document_ID.exec list -> unit
    1.10    val reset: unit -> Future.group list
    1.11 @@ -147,6 +148,14 @@
    1.12        | NONE => raise Fail (unregistered exec_id))
    1.13      end));
    1.14  
    1.15 +fun print_report s =
    1.16 +  if s = "" orelse not (Multithreading.enabled ()) then Output.direct_report s
    1.17 +  else
    1.18 +    let
    1.19 +      val body = YXML.parse_body s  (*sharable closure!*)
    1.20 +      val params = {name = "", pos = Position.thread_data (), pri = 0};
    1.21 +    in print params (fn _ => Output.direct_report (YXML.string_of_body body)) end;
    1.22 +
    1.23  fun fork_prints exec_id =
    1.24    (case Inttab.lookup (#2 (get_state ())) exec_id of
    1.25      SOME (_, prints) =>