support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
authorwenzelm
Mon Mar 31 10:28:08 2014 +0200 (2014-03-31 ago)
changeset 5633338f1422ef473
parent 56327 3e62e68fb342
child 56334 6b3739fee456
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/Pure/Concurrent/future.ML
src/Pure/General/output.ML
src/Pure/General/position.ML
src/Pure/General/timing.ML
src/Pure/Isar/args.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/query_operation.ML
src/Pure/PIDE/resources.ML
src/Pure/PIDE/session.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/System/invoke_scala.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/message_channel.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/proof_general.ML
src/Pure/Tools/simplifier_trace.ML
src/Pure/context_position.ML
src/Pure/skip_proof.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun Mar 30 21:24:59 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Mar 31 10:28:08 2014 +0200
     1.3 @@ -505,6 +505,6 @@
     1.4      let
     1.5        val this_thy = @{theory}
     1.6        val provers = space_implode " " (#provers (default_params this_thy []))
     1.7 -    in Output.protocol_message Markup.sledgehammer_provers provers end)
     1.8 +    in Output.protocol_message Markup.sledgehammer_provers [provers] end)
     1.9  
    1.10  end;
     2.1 --- a/src/Pure/Concurrent/future.ML	Sun Mar 30 21:24:59 2014 +0200
     2.2 +++ b/src/Pure/Concurrent/future.ML	Mon Mar 31 10:28:08 2014 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     2.5    val cancel_group: group -> unit
     2.6    val cancel: 'a future -> unit
     2.7 -  val error_msg: Position.T -> (serial * string) * string option -> unit
     2.8 +  val error_message: Position.T -> (serial * string) * string option -> unit
     2.9    val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
    2.10    type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
    2.11    val default_params: params
    2.12 @@ -210,7 +210,7 @@
    2.13          ("workers_active", Markup.print_int active),
    2.14          ("workers_waiting", Markup.print_int waiting)] @
    2.15          ML_Statistics.get ();
    2.16 -    in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
    2.17 +    in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
    2.18    else ();
    2.19  
    2.20  
    2.21 @@ -257,7 +257,7 @@
    2.22            fold (fn job => fn ok => job valid andalso ok) jobs true) ());
    2.23      val _ =
    2.24        if ! Multithreading.trace >= 2 then
    2.25 -        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
    2.26 +        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) []
    2.27        else ();
    2.28      val _ = SYNCHRONIZED "finish" (fn () =>
    2.29        let
    2.30 @@ -434,7 +434,7 @@
    2.31  
    2.32  (* results *)
    2.33  
    2.34 -fun error_msg pos ((serial, msg), exec_id) =
    2.35 +fun error_message pos ((serial, msg), exec_id) =
    2.36    Position.setmp_thread_data pos (fn () =>
    2.37      let val id = Position.get_id pos in
    2.38        if is_none id orelse is_none exec_id orelse id = exec_id
     3.1 --- a/src/Pure/General/output.ML	Sun Mar 30 21:24:59 2014 +0200
     3.2 +++ b/src/Pure/General/output.ML	Mon Mar 31 10:28:08 2014 +0200
     3.3 @@ -30,25 +30,25 @@
     3.4    val error_message: string -> unit
     3.5    val prompt: string -> unit
     3.6    val status: string -> unit
     3.7 -  val report: string -> unit
     3.8 -  val result: Properties.T -> string -> unit
     3.9 -  val protocol_message: Properties.T -> string -> unit
    3.10 -  val try_protocol_message: Properties.T -> string -> unit
    3.11 +  val report: string list -> unit
    3.12 +  val result: Properties.T -> string list -> unit
    3.13 +  val protocol_message: Properties.T -> string list -> unit
    3.14 +  val try_protocol_message: Properties.T -> string list -> unit
    3.15  end;
    3.16  
    3.17  signature PRIVATE_OUTPUT =
    3.18  sig
    3.19    include OUTPUT
    3.20 -  val writeln_fn: (output -> unit) Unsynchronized.ref
    3.21 -  val urgent_message_fn: (output -> unit) Unsynchronized.ref
    3.22 -  val tracing_fn: (output -> unit) Unsynchronized.ref
    3.23 -  val warning_fn: (output -> unit) Unsynchronized.ref
    3.24 -  val error_message_fn: (serial * output -> unit) Unsynchronized.ref
    3.25 +  val writeln_fn: (output list -> unit) Unsynchronized.ref
    3.26 +  val urgent_message_fn: (output list -> unit) Unsynchronized.ref
    3.27 +  val tracing_fn: (output list -> unit) Unsynchronized.ref
    3.28 +  val warning_fn: (output list -> unit) Unsynchronized.ref
    3.29 +  val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    3.30    val prompt_fn: (output -> unit) Unsynchronized.ref
    3.31 -  val status_fn: (output -> unit) Unsynchronized.ref
    3.32 -  val report_fn: (output -> unit) Unsynchronized.ref
    3.33 -  val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    3.34 -  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    3.35 +  val status_fn: (output list -> unit) Unsynchronized.ref
    3.36 +  val report_fn: (output list -> unit) Unsynchronized.ref
    3.37 +  val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    3.38 +  val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    3.39  end;
    3.40  
    3.41  structure Output: PRIVATE_OUTPUT =
    3.42 @@ -94,31 +94,31 @@
    3.43  
    3.44  exception Protocol_Message of Properties.T;
    3.45  
    3.46 -val writeln_fn = Unsynchronized.ref physical_writeln;
    3.47 -val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
    3.48 -val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    3.49 -val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
    3.50 +val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
    3.51 +val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);  (*Proof General legacy*)
    3.52 +val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    3.53 +val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    3.54  val error_message_fn =
    3.55 -  Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
    3.56 -val prompt_fn = Unsynchronized.ref physical_stdout;
    3.57 -val status_fn = Unsynchronized.ref (fn _: output => ());
    3.58 -val report_fn = Unsynchronized.ref (fn _: output => ());
    3.59 -val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
    3.60 -val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    3.61 +  Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    3.62 +val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
    3.63 +val status_fn = Unsynchronized.ref (fn _: output list => ());
    3.64 +val report_fn = Unsynchronized.ref (fn _: output list => ());
    3.65 +val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
    3.66 +val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
    3.67    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    3.68  
    3.69 -fun writeln s = ! writeln_fn (output s);
    3.70 -fun urgent_message s = ! urgent_message_fn (output s);  (*Proof General legacy*)
    3.71 -fun tracing s = ! tracing_fn (output s);
    3.72 -fun warning s = ! warning_fn (output s);
    3.73 -fun error_message' (i, s) = ! error_message_fn (i, output s);
    3.74 +fun writeln s = ! writeln_fn [output s];
    3.75 +fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
    3.76 +fun tracing s = ! tracing_fn [output s];
    3.77 +fun warning s = ! warning_fn [output s];
    3.78 +fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    3.79  fun error_message s = error_message' (serial (), s);
    3.80  fun prompt s = ! prompt_fn (output s);
    3.81 -fun status s = ! status_fn (output s);
    3.82 -fun report s = ! report_fn (output s);
    3.83 -fun result props s = ! result_fn props (output s);
    3.84 -fun protocol_message props s = ! protocol_message_fn props (output s);
    3.85 -fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
    3.86 +fun status s = ! status_fn [output s];
    3.87 +fun report ss = ! report_fn (map output ss);
    3.88 +fun result props ss = ! result_fn props (map output ss);
    3.89 +fun protocol_message props ss = ! protocol_message_fn props (map output ss);
    3.90 +fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
    3.91  
    3.92  end;
    3.93  
     4.1 --- a/src/Pure/General/position.ML	Sun Mar 30 21:24:59 2014 +0200
     4.2 +++ b/src/Pure/General/position.ML	Mon Mar 31 10:28:08 2014 +0200
     4.3 @@ -166,7 +166,7 @@
     4.4  fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
     4.5  
     4.6  fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
     4.7 -fun report_text pos markup txt = Output.report (reported_text pos markup txt);
     4.8 +fun report_text pos markup txt = Output.report [reported_text pos markup txt];
     4.9  fun report pos markup = report_text pos markup "";
    4.10  
    4.11  type report = T * Markup.T;
    4.12 @@ -174,7 +174,7 @@
    4.13  
    4.14  val reports_text =
    4.15    map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
    4.16 -  #> implode #> Output.report;
    4.17 +  #> Output.report;
    4.18  
    4.19  val reports = map (rpair "") #> reports_text;
    4.20  
     5.1 --- a/src/Pure/General/timing.ML	Sun Mar 30 21:24:59 2014 +0200
     5.2 +++ b/src/Pure/General/timing.ML	Mon Mar 31 10:28:08 2014 +0200
     5.3 @@ -105,7 +105,7 @@
     5.4  fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
     5.5  
     5.6  fun protocol_message props t =
     5.7 -  Output.try_protocol_message (props @ Markup.timing_properties t) "";
     5.8 +  Output.try_protocol_message (props @ Markup.timing_properties t) [];
     5.9  
    5.10  fun protocol props f x =
    5.11    let
     6.1 --- a/src/Pure/Isar/args.ML	Sun Mar 30 21:24:59 2014 +0200
     6.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 31 10:28:08 2014 +0200
     6.3 @@ -277,8 +277,7 @@
     6.4        if Context_Position.is_visible_generic context then
     6.5          ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
     6.6          |> map (fn (p, m) => Position.reported_text p m "")
     6.7 -        |> implode
     6.8 -      else "";
     6.9 +      else [];
    6.10    in
    6.11      (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
    6.12        (SOME x, (context', [])) =>
    6.13 @@ -294,7 +293,7 @@
    6.14              if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2);
    6.15          in
    6.16            error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
    6.17 -            Markup.markup_report (reported_text ()))
    6.18 +            Markup.markup_report (implode (reported_text ())))
    6.19          end)
    6.20    end;
    6.21  
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 30 21:24:59 2014 +0200
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 31 10:28:08 2014 +0200
     7.3 @@ -716,7 +716,7 @@
     7.4  (* proof navigation *)
     7.5  
     7.6  fun report_back () =
     7.7 -  Output.report (Markup.markup Markup.bad "Explicit backtracking");
     7.8 +  Output.report [Markup.markup Markup.bad "Explicit backtracking"];
     7.9  
    7.10  val _ =
    7.11    Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
     8.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 30 21:24:59 2014 +0200
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Mar 31 10:28:08 2014 +0200
     8.3 @@ -78,8 +78,8 @@
     8.4    val read_arity: Proof.context -> xstring * string list * string -> arity
     8.5    val cert_arity: Proof.context -> arity -> arity
     8.6    val allow_dummies: Proof.context -> Proof.context
     8.7 -  val prepare_sortsT: Proof.context -> typ list -> string * typ list
     8.8 -  val prepare_sorts: Proof.context -> term list -> string * term list
     8.9 +  val prepare_sortsT: Proof.context -> typ list -> string list * typ list
    8.10 +  val prepare_sorts: Proof.context -> term list -> string list * term list
    8.11    val check_tfree: Proof.context -> string * sort -> string * sort
    8.12    val read_term_pattern: Proof.context -> string -> term
    8.13    val read_term_schematic: Proof.context -> string -> term
    8.14 @@ -691,7 +691,7 @@
    8.15              | TVar (xi, raw_S) => get_sort_reports xi raw_S
    8.16              | _ => I)) tys [];
    8.17  
    8.18 -  in (implode (map #2 reports), get_sort) end;
    8.19 +  in (map #2 reports, get_sort) end;
    8.20  
    8.21  fun replace_sortsT get_sort =
    8.22    map_atyps
     9.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Sun Mar 30 21:24:59 2014 +0200
     9.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Mar 31 10:28:08 2014 +0200
     9.3 @@ -55,7 +55,7 @@
     9.4      fun output () =
     9.5        persistent_reports
     9.6        |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
     9.7 -      |> implode |> Output.report;
     9.8 +      |> Output.report;
     9.9    in
    9.10      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
    9.11      then
    10.1 --- a/src/Pure/PIDE/command.ML	Sun Mar 30 21:24:59 2014 +0200
    10.2 +++ b/src/Pure/PIDE/command.ML	Mon Mar 31 10:28:08 2014 +0200
    10.3 @@ -199,7 +199,7 @@
    10.4              else Runtime.exn_messages_ids exn)) ();
    10.5  
    10.6  fun report tr m =
    10.7 -  Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
    10.8 +  Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
    10.9  
   10.10  fun status tr m =
   10.11    Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
   10.12 @@ -223,7 +223,7 @@
   10.13        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   10.14        val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   10.15        val errs = errs1 @ errs2;
   10.16 -      val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   10.17 +      val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   10.18      in
   10.19        (case result of
   10.20          NONE =>
   10.21 @@ -279,7 +279,7 @@
   10.22    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
   10.23      handle exn =>
   10.24        if Exn.is_interrupt exn then reraise exn
   10.25 -      else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
   10.26 +      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
   10.27  
   10.28  fun print_finished (Print {print_process, ...}) = memo_finished print_process;
   10.29  
    11.1 --- a/src/Pure/PIDE/execution.ML	Sun Mar 30 21:24:59 2014 +0200
    11.2 +++ b/src/Pure/PIDE/execution.ML	Mon Mar 31 10:28:08 2014 +0200
    11.3 @@ -122,9 +122,9 @@
    11.4                    Exn.Exn exn =>
    11.5                     (status task [Markup.failed];
    11.6                      status task [Markup.finished];
    11.7 -                    Output.report (Markup.markup_only Markup.bad);
    11.8 +                    Output.report [Markup.markup_only Markup.bad];
    11.9                      if exec_id = 0 then ()
   11.10 -                    else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
   11.11 +                    else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
   11.12                  | Exn.Res _ =>
   11.13                      status task [Markup.finished])
   11.14              in Exn.release result end);
    12.1 --- a/src/Pure/PIDE/protocol.ML	Sun Mar 30 21:24:59 2014 +0200
    12.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Mar 31 10:28:08 2014 +0200
    12.3 @@ -85,10 +85,10 @@
    12.4  
    12.5          val _ =
    12.6            Output.protocol_message Markup.assign_update
    12.7 -            ((new_id, assign_update) |>
    12.8 +            [(new_id, assign_update) |>
    12.9                let open XML.Encode
   12.10                in pair int (list (pair int (list int))) end
   12.11 -              |> YXML.string_of_body);
   12.12 +              |> YXML.string_of_body];
   12.13        in Document.start_execution state' end));
   12.14  
   12.15  val _ =
   12.16 @@ -99,7 +99,7 @@
   12.17            YXML.parse_body versions_yxml |>
   12.18              let open XML.Decode in list int end;
   12.19          val state1 = Document.remove_versions versions state;
   12.20 -        val _ = Output.protocol_message Markup.removed_versions versions_yxml;
   12.21 +        val _ = Output.protocol_message Markup.removed_versions [versions_yxml];
   12.22        in state1 end));
   12.23  
   12.24  val _ =
    13.1 --- a/src/Pure/PIDE/query_operation.ML	Sun Mar 30 21:24:59 2014 +0200
    13.2 +++ b/src/Pure/PIDE/query_operation.ML	Mon Mar 31 10:28:08 2014 +0200
    13.3 @@ -20,7 +20,7 @@
    13.4          SOME {delay = NONE, pri = 0, persistent = false, strict = false,
    13.5            print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    13.6              let
    13.7 -              fun result s = Output.result [(Markup.instanceN, instance)] s;
    13.8 +              fun result s = Output.result [(Markup.instanceN, instance)] [s];
    13.9                fun status m = result (Markup.markup_only m);
   13.10                fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
   13.11                fun toplevel_error exn =
    14.1 --- a/src/Pure/PIDE/resources.ML	Sun Mar 30 21:24:59 2014 +0200
    14.2 +++ b/src/Pure/PIDE/resources.ML	Mon Mar 31 10:28:08 2014 +0200
    14.3 @@ -213,7 +213,7 @@
    14.4            if strict then error msg
    14.5            else if Context_Position.is_visible ctxt then
    14.6              Output.report
    14.7 -              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
    14.8 +              [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
    14.9            else ()
   14.10          end;
   14.11    in path end;
    15.1 --- a/src/Pure/PIDE/session.ML	Sun Mar 30 21:24:59 2014 +0200
    15.2 +++ b/src/Pure/PIDE/session.ML	Mon Mar 31 10:28:08 2014 +0200
    15.3 @@ -68,13 +68,13 @@
    15.4  
    15.5  fun protocol_handler name =
    15.6    Synchronized.change protocol_handlers (fn handlers =>
    15.7 -   (Output.try_protocol_message (Markup.protocol_handler name) "";
    15.8 +   (Output.try_protocol_message (Markup.protocol_handler name) [];
    15.9      if not (member (op =) handlers name) then ()
   15.10      else warning ("Redefining protocol handler: " ^ quote name);
   15.11      update (op =) name handlers));
   15.12  
   15.13  fun init_protocol_handlers () =
   15.14    Synchronized.value protocol_handlers
   15.15 -  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
   15.16 +  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
   15.17  
   15.18  end;
    16.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Mar 30 21:24:59 2014 +0200
    16.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Mar 31 10:28:08 2014 +0200
    16.3 @@ -949,11 +949,10 @@
    16.4          if Position.is_reported pos then
    16.5            cons (Position.reported_text pos Markup.typing
    16.6              (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
    16.7 -        else I) ps tys' []
    16.8 -      |> implode;
    16.9 +        else I) ps tys' [];
   16.10  
   16.11      val _ =
   16.12 -      if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report)
   16.13 +      if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report)
   16.14        else ();
   16.15    in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
   16.16  
    17.1 --- a/src/Pure/System/invoke_scala.ML	Sun Mar 30 21:24:59 2014 +0200
    17.2 +++ b/src/Pure/System/invoke_scala.ML	Mon Mar 31 10:28:08 2014 +0200
    17.3 @@ -30,10 +30,10 @@
    17.4  fun promise_method name arg =
    17.5    let
    17.6      val id = new_id ();
    17.7 -    fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
    17.8 +    fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    17.9      val promise = Future.promise abort : string future;
   17.10      val _ = Synchronized.change promises (Symtab.update (id, promise));
   17.11 -    val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
   17.12 +    val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
   17.13    in promise end;
   17.14  
   17.15  fun method name arg = Future.join (promise_method name arg);
    18.1 --- a/src/Pure/System/isabelle_process.ML	Sun Mar 30 21:24:59 2014 +0200
    18.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Mar 31 10:28:08 2014 +0200
    18.3 @@ -106,7 +106,7 @@
    18.4        Message_Channel.send msg_channel (Message_Channel.message name props body);
    18.5  
    18.6      fun standard_message props name body =
    18.7 -      if body = "" then ()
    18.8 +      if forall (fn s => s = "") body then ()
    18.9        else
   18.10          message name
   18.11            (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
   18.12 @@ -124,7 +124,7 @@
   18.13      Output.protocol_message_fn := message Markup.protocolN;
   18.14      Output.urgent_message_fn := ! Output.writeln_fn;
   18.15      Output.prompt_fn := ignore;
   18.16 -    message Markup.initN [] (Session.welcome ());
   18.17 +    message Markup.initN [] [Session.welcome ()];
   18.18      msg_channel
   18.19    end;
   18.20  
    19.1 --- a/src/Pure/System/message_channel.ML	Sun Mar 30 21:24:59 2014 +0200
    19.2 +++ b/src/Pure/System/message_channel.ML	Mon Mar 31 10:28:08 2014 +0200
    19.3 @@ -7,7 +7,7 @@
    19.4  signature MESSAGE_CHANNEL =
    19.5  sig
    19.6    type message
    19.7 -  val message: string -> Properties.T -> string -> message
    19.8 +  val message: string -> Properties.T -> string list -> message
    19.9    type T
   19.10    val send: T -> message -> unit
   19.11    val shutdown: T -> unit
   19.12 @@ -21,13 +21,14 @@
   19.13  
   19.14  datatype message = Message of string list;
   19.15  
   19.16 -fun chunk s = [string_of_int (size s), "\n", s];
   19.17 +fun chunk ss =
   19.18 +  string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
   19.19  
   19.20  fun message name raw_props body =
   19.21    let
   19.22      val robust_props = map (pairself YXML.embed_controls) raw_props;
   19.23      val header = YXML.string_of (XML.Elem ((name, robust_props), []));
   19.24 -  in Message (chunk header @ chunk body) end;
   19.25 +  in Message (chunk [header] @ chunk body) end;
   19.26  
   19.27  fun output_message channel (Message ss) =
   19.28    List.app (System_Channel.output channel) ss;
   19.29 @@ -37,7 +38,7 @@
   19.30  
   19.31  fun flush channel = ignore (try System_Channel.flush channel);
   19.32  
   19.33 -val flush_message = message Markup.protocolN Markup.flush "";
   19.34 +val flush_message = message Markup.protocolN Markup.flush [];
   19.35  fun flush_output channel = (output_message channel flush_message; flush channel);
   19.36  
   19.37  
    20.1 --- a/src/Pure/Thy/thy_info.ML	Sun Mar 30 21:24:59 2014 +0200
    20.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Mar 31 10:28:08 2014 +0200
    20.3 @@ -269,7 +269,7 @@
    20.4    let
    20.5      val _ = kill_thy name;
    20.6      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
    20.7 -    val _ = Output.try_protocol_message (Markup.loading_theory name) "";
    20.8 +    val _ = Output.try_protocol_message (Markup.loading_theory name) [];
    20.9  
   20.10      val {master = (thy_path, _), imports} = deps;
   20.11      val dir = Path.dir thy_path;
    21.1 --- a/src/Pure/Tools/proof_general.ML	Sun Mar 30 21:24:59 2014 +0200
    21.2 +++ b/src/Pure/Tools/proof_general.ML	Mon Mar 31 10:28:08 2014 +0200
    21.3 @@ -258,8 +258,8 @@
    21.4  
    21.5  (* hooks *)
    21.6  
    21.7 -fun message bg en prfx text =
    21.8 -  (case render text of
    21.9 +fun message bg en prfx body =
   21.10 +  (case render (implode body) of
   21.11      "" => ()
   21.12    | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
   21.13  
   21.14 @@ -276,7 +276,7 @@
   21.15  
   21.16  (* notification *)
   21.17  
   21.18 -val emacs_notify = message (special "I") (special "J") "";
   21.19 +fun emacs_notify s = message (special "I") (special "J") "" [s];
   21.20  
   21.21  fun tell_clear_goals () =
   21.22    emacs_notify "Proof General, please clear the goals buffer.";
    22.1 --- a/src/Pure/Tools/simplifier_trace.ML	Sun Mar 30 21:24:59 2014 +0200
    22.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Mar 31 10:28:08 2014 +0200
    22.3 @@ -133,7 +133,7 @@
    22.4  (** markup **)
    22.5  
    22.6  fun output_result (id, data) =
    22.7 -  Output.result (Markup.serial_properties id) data
    22.8 +  Output.result (Markup.serial_properties id) [data]
    22.9  
   22.10  val parentN = "parent"
   22.11  val textN = "text"
   22.12 @@ -184,7 +184,7 @@
   22.13  fun send_request (result_id, content) =
   22.14    let
   22.15      fun break () =
   22.16 -      (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
   22.17 +      (Output.protocol_message (Markup.simp_trace_cancel result_id) [];
   22.18         Synchronized.change futures (Inttab.delete_safe result_id))
   22.19      val promise = Future.promise break : string future
   22.20    in
    23.1 --- a/src/Pure/context_position.ML	Sun Mar 30 21:24:59 2014 +0200
    23.2 +++ b/src/Pure/context_position.ML	Mon Mar 31 10:28:08 2014 +0200
    23.3 @@ -49,13 +49,13 @@
    23.4  
    23.5  fun report_generic context pos markup =
    23.6    if is_reported_generic context pos then
    23.7 -    Output.report (Position.reported_text pos markup "")
    23.8 +    Output.report [Position.reported_text pos markup ""]
    23.9    else ();
   23.10  
   23.11  fun reported_text ctxt pos markup txt =
   23.12    if is_reported ctxt pos then Position.reported_text pos markup txt else "";
   23.13  
   23.14 -fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
   23.15 +fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt];
   23.16  fun report ctxt pos markup = report_text ctxt pos markup "";
   23.17  
   23.18  fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else ();
    24.1 --- a/src/Pure/skip_proof.ML	Sun Mar 30 21:24:59 2014 +0200
    24.2 +++ b/src/Pure/skip_proof.ML	Mon Mar 31 10:28:08 2014 +0200
    24.3 @@ -19,7 +19,7 @@
    24.4  
    24.5  fun report ctxt =
    24.6    if Context_Position.is_visible ctxt then
    24.7 -    Output.report (Markup.markup Markup.bad "Skipped proof")
    24.8 +    Output.report [Markup.markup Markup.bad "Skipped proof"]
    24.9    else ();
   24.10  
   24.11