support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
authorwenzelm
Wed Mar 26 20:32:15 2014 +0100 (2014-03-26 ago)
changeset 562973925634718fb
parent 56296 5413b6379c0e
child 56298 cf7710540f39
support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
src/Pure/General/output.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/General/output.ML	Wed Mar 26 20:08:07 2014 +0100
     1.2 +++ b/src/Pure/General/output.ML	Wed Mar 26 20:32:15 2014 +0100
     1.3 @@ -30,6 +30,8 @@
     1.4    val error_message: string -> unit
     1.5    val prompt: string -> unit
     1.6    val status: string -> unit
     1.7 +  val direct_report: string -> unit
     1.8 +  val redirect_report: (string -> unit) -> ('a -> 'b) -> 'a -> 'b
     1.9    val report: string -> unit
    1.10    val result: Properties.T -> string -> unit
    1.11    val protocol_message: Properties.T -> string -> unit
    1.12 @@ -115,7 +117,17 @@
    1.13  fun error_message s = error_message' (serial (), s);
    1.14  fun prompt s = ! prompt_fn (output s);
    1.15  fun status s = ! status_fn (output s);
    1.16 -fun report s = ! report_fn (output s);
    1.17 +
    1.18 +fun direct_report s = ! report_fn (output s);
    1.19 +
    1.20 +local
    1.21 +  val tag = Universal.tag () : (string -> unit) Universal.tag;
    1.22 +  fun thread_data () = the_default direct_report (Thread.getLocal tag);
    1.23 +in
    1.24 +  fun redirect_report rep = Library.setmp_thread_data tag (thread_data ()) rep;
    1.25 +  fun report s = thread_data () s;
    1.26 +end;
    1.27 +
    1.28  fun result props s = ! result_fn props (output s);
    1.29  fun protocol_message props s = ! protocol_message_fn props (output s);
    1.30  fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
     2.1 --- a/src/Pure/PIDE/execution.ML	Wed Mar 26 20:08:07 2014 +0100
     2.2 +++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 20:32:15 2014 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4    type params = {name: string, pos: Position.T, pri: int}
     2.5    val fork: params -> (unit -> 'a) -> 'a future
     2.6    val print: params -> (serial -> unit) -> unit
     2.7 +  val print_report: string -> unit
     2.8    val fork_prints: Document_ID.exec -> unit
     2.9    val purge: Document_ID.exec list -> unit
    2.10    val reset: unit -> Future.group list
    2.11 @@ -147,6 +148,14 @@
    2.12        | NONE => raise Fail (unregistered exec_id))
    2.13      end));
    2.14  
    2.15 +fun print_report s =
    2.16 +  if s = "" orelse not (Multithreading.enabled ()) then Output.direct_report s
    2.17 +  else
    2.18 +    let
    2.19 +      val body = YXML.parse_body s  (*sharable closure!*)
    2.20 +      val params = {name = "", pos = Position.thread_data (), pri = 0};
    2.21 +    in print params (fn _ => Output.direct_report (YXML.string_of_body body)) end;
    2.22 +
    2.23  fun fork_prints exec_id =
    2.24    (case Inttab.lookup (#2 (get_state ())) exec_id of
    2.25      SOME (_, prints) =>