# HG changeset patch # User wenzelm # Date 1396254488 -7200 # Node ID 38f1422ef473d97b7a2864d57844985bbd7bd7a8 # Parent 3e62e68fb342cce5d42dc266d3d3741322e375ea 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; diff -r 3e62e68fb342 -r 38f1422ef473 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Mar 31 10:28:08 2014 +0200 @@ -505,6 +505,6 @@ let val this_thy = @{theory} val provers = space_implode " " (#provers (default_params this_thy [])) - in Output.protocol_message Markup.sledgehammer_provers provers end) + in Output.protocol_message Markup.sledgehammer_provers [provers] end) end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Concurrent/future.ML Mon Mar 31 10:28:08 2014 +0200 @@ -56,7 +56,7 @@ val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: group -> unit val cancel: 'a future -> unit - val error_msg: Position.T -> (serial * string) * string option -> unit + val error_message: Position.T -> (serial * string) * string option -> unit val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool} val default_params: params @@ -210,7 +210,7 @@ ("workers_active", Markup.print_int active), ("workers_waiting", Markup.print_int waiting)] @ ML_Statistics.get (); - in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end + in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end else (); @@ -257,7 +257,7 @@ fold (fn job => fn ok => job valid andalso ok) jobs true) ()); val _ = if ! Multithreading.trace >= 2 then - Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) "" + Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) [] else (); val _ = SYNCHRONIZED "finish" (fn () => let @@ -434,7 +434,7 @@ (* results *) -fun error_msg pos ((serial, msg), exec_id) = +fun error_message pos ((serial, msg), exec_id) = Position.setmp_thread_data pos (fn () => let val id = Position.get_id pos in if is_none id orelse is_none exec_id orelse id = exec_id diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/General/output.ML Mon Mar 31 10:28:08 2014 +0200 @@ -30,25 +30,25 @@ val error_message: string -> unit val prompt: string -> unit val status: string -> unit - val report: string -> unit - val result: Properties.T -> string -> unit - val protocol_message: Properties.T -> string -> unit - val try_protocol_message: Properties.T -> string -> unit + val report: string list -> unit + val result: Properties.T -> string list -> unit + val protocol_message: Properties.T -> string list -> unit + val try_protocol_message: Properties.T -> string list -> unit end; signature PRIVATE_OUTPUT = sig include OUTPUT - val writeln_fn: (output -> unit) Unsynchronized.ref - val urgent_message_fn: (output -> unit) Unsynchronized.ref - val tracing_fn: (output -> unit) Unsynchronized.ref - val warning_fn: (output -> unit) Unsynchronized.ref - val error_message_fn: (serial * output -> unit) Unsynchronized.ref + val writeln_fn: (output list -> unit) Unsynchronized.ref + val urgent_message_fn: (output list -> unit) Unsynchronized.ref + val tracing_fn: (output list -> unit) Unsynchronized.ref + val warning_fn: (output list -> unit) Unsynchronized.ref + val error_message_fn: (serial * output list -> unit) Unsynchronized.ref val prompt_fn: (output -> unit) Unsynchronized.ref - val status_fn: (output -> unit) Unsynchronized.ref - val report_fn: (output -> unit) Unsynchronized.ref - val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref - val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref + val status_fn: (output list -> unit) Unsynchronized.ref + val report_fn: (output list -> unit) Unsynchronized.ref + val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref + val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref end; structure Output: PRIVATE_OUTPUT = @@ -94,31 +94,31 @@ exception Protocol_Message of Properties.T; -val writeln_fn = Unsynchronized.ref physical_writeln; -val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*) -val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s); -val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### "); +val writeln_fn = Unsynchronized.ref (physical_writeln o implode); +val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*) +val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); +val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode); val error_message_fn = - Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s)); -val prompt_fn = Unsynchronized.ref physical_stdout; -val status_fn = Unsynchronized.ref (fn _: output => ()); -val report_fn = Unsynchronized.ref (fn _: output => ()); -val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ()); -val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = + Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss))); +val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*) +val status_fn = Unsynchronized.ref (fn _: output list => ()); +val report_fn = Unsynchronized.ref (fn _: output list => ()); +val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ()); +val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref = Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props); -fun writeln s = ! writeln_fn (output s); -fun urgent_message s = ! urgent_message_fn (output s); (*Proof General legacy*) -fun tracing s = ! tracing_fn (output s); -fun warning s = ! warning_fn (output s); -fun error_message' (i, s) = ! error_message_fn (i, output s); +fun writeln s = ! writeln_fn [output s]; +fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*) +fun tracing s = ! tracing_fn [output s]; +fun warning s = ! warning_fn [output s]; +fun error_message' (i, s) = ! error_message_fn (i, [output s]); 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 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 _ => (); +fun status s = ! status_fn [output s]; +fun report ss = ! report_fn (map output ss); +fun result props ss = ! result_fn props (map output ss); +fun protocol_message props ss = ! protocol_message_fn props (map output ss); +fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => (); end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/General/position.ML Mon Mar 31 10:28:08 2014 +0200 @@ -166,7 +166,7 @@ fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos); fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else ""; -fun report_text pos markup txt = Output.report (reported_text pos markup txt); +fun report_text pos markup txt = Output.report [reported_text pos markup txt]; fun report pos markup = report_text pos markup ""; type report = T * Markup.T; @@ -174,7 +174,7 @@ val reports_text = map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "") - #> implode #> Output.report; + #> Output.report; val reports = map (rpair "") #> reports_text; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/General/timing.ML Mon Mar 31 10:28:08 2014 +0200 @@ -105,7 +105,7 @@ fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); fun protocol_message props t = - Output.try_protocol_message (props @ Markup.timing_properties t) ""; + Output.try_protocol_message (props @ Markup.timing_properties t) []; fun protocol props f x = let diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Isar/args.ML Mon Mar 31 10:28:08 2014 +0200 @@ -277,8 +277,7 @@ if Context_Position.is_visible_generic context then ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1) |> map (fn (p, m) => Position.reported_text p m "") - |> implode - else ""; + else []; in (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of (SOME x, (context', [])) => @@ -294,7 +293,7 @@ if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2); in error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ - Markup.markup_report (reported_text ())) + Markup.markup_report (implode (reported_text ()))) end) end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon Mar 31 10:28:08 2014 +0200 @@ -716,7 +716,7 @@ (* proof navigation *) fun report_back () = - Output.report (Markup.markup Markup.bad "Explicit backtracking"); + Output.report [Markup.markup Markup.bad "Explicit backtracking"]; val _ = Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command" diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Mar 31 10:28:08 2014 +0200 @@ -78,8 +78,8 @@ val read_arity: Proof.context -> xstring * string list * string -> arity val cert_arity: Proof.context -> arity -> arity val allow_dummies: Proof.context -> Proof.context - val prepare_sortsT: Proof.context -> typ list -> string * typ list - val prepare_sorts: Proof.context -> term list -> string * term list + val prepare_sortsT: Proof.context -> typ list -> string list * typ list + val prepare_sorts: Proof.context -> term list -> string list * term list val check_tfree: Proof.context -> string * sort -> string * sort val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term @@ -691,7 +691,7 @@ | TVar (xi, raw_S) => get_sort_reports xi raw_S | _ => I)) tys []; - in (implode (map #2 reports), get_sort) end; + in (map #2 reports, get_sort) end; fun replace_sortsT get_sort = map_atyps diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Mar 31 10:28:08 2014 +0200 @@ -55,7 +55,7 @@ fun output () = persistent_reports |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) - |> implode |> Output.report; + |> Output.report; in if not (null persistent_reports) andalso redirect andalso Multithreading.enabled () then diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/PIDE/command.ML Mon Mar 31 10:28:08 2014 +0200 @@ -199,7 +199,7 @@ else Runtime.exn_messages_ids exn)) (); fun report tr m = - Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) (); + Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); fun status tr m = Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); @@ -223,7 +223,7 @@ val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); val errs = errs1 @ errs2; - val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; + val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; in (case result of NONE => @@ -279,7 +279,7 @@ (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () handle exn => if Exn.is_interrupt exn then reraise exn - else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn); + else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn); fun print_finished (Print {print_process, ...}) = memo_finished print_process; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/PIDE/execution.ML Mon Mar 31 10:28:08 2014 +0200 @@ -122,9 +122,9 @@ Exn.Exn exn => (status task [Markup.failed]; status task [Markup.finished]; - Output.report (Markup.markup_only Markup.bad); + Output.report [Markup.markup_only Markup.bad]; if exec_id = 0 then () - else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn)) + else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn)) | Exn.Res _ => status task [Markup.finished]) in Exn.release result end); diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/PIDE/protocol.ML Mon Mar 31 10:28:08 2014 +0200 @@ -85,10 +85,10 @@ val _ = Output.protocol_message Markup.assign_update - ((new_id, assign_update) |> + [(new_id, assign_update) |> let open XML.Encode in pair int (list (pair int (list int))) end - |> YXML.string_of_body); + |> YXML.string_of_body]; in Document.start_execution state' end)); val _ = @@ -99,7 +99,7 @@ YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; - val _ = Output.protocol_message Markup.removed_versions versions_yxml; + val _ = Output.protocol_message Markup.removed_versions [versions_yxml]; in state1 end)); val _ = diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/PIDE/query_operation.ML --- a/src/Pure/PIDE/query_operation.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/PIDE/query_operation.ML Mon Mar 31 10:28:08 2014 +0200 @@ -20,7 +20,7 @@ SOME {delay = NONE, pri = 0, persistent = false, strict = false, print_fn = fn _ => uninterruptible (fn restore_attributes => fn state => let - fun result s = Output.result [(Markup.instanceN, instance)] s; + fun result s = Output.result [(Markup.instanceN, instance)] [s]; fun status m = result (Markup.markup_only m); fun output_result s = result (Markup.markup (Markup.writelnN, []) s); fun toplevel_error exn = diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/PIDE/resources.ML Mon Mar 31 10:28:08 2014 +0200 @@ -213,7 +213,7 @@ if strict then error msg else if Context_Position.is_visible ctxt then Output.report - (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg) + [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg] else () end; in path end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/PIDE/session.ML Mon Mar 31 10:28:08 2014 +0200 @@ -68,13 +68,13 @@ fun protocol_handler name = Synchronized.change protocol_handlers (fn handlers => - (Output.try_protocol_message (Markup.protocol_handler name) ""; + (Output.try_protocol_message (Markup.protocol_handler name) []; if not (member (op =) handlers name) then () else warning ("Redefining protocol handler: " ^ quote name); update (op =) name handlers)); fun init_protocol_handlers () = Synchronized.value protocol_handlers - |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) ""); + |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []); end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Mon Mar 31 10:28:08 2014 +0200 @@ -949,11 +949,10 @@ if Position.is_reported pos then cons (Position.reported_text pos Markup.typing (Syntax.string_of_typ ctxt (Logic.dest_type ty))) - else I) ps tys' [] - |> implode; + else I) ps tys' []; val _ = - if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report) + if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report) else (); in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/System/invoke_scala.ML --- a/src/Pure/System/invoke_scala.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/System/invoke_scala.ML Mon Mar 31 10:28:08 2014 +0200 @@ -30,10 +30,10 @@ fun promise_method name arg = let val id = new_id (); - fun abort () = Output.protocol_message (Markup.cancel_scala id) ""; + fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); - val _ = Output.protocol_message (Markup.invoke_scala name id) arg; + val _ = Output.protocol_message (Markup.invoke_scala name id) [arg]; in promise end; fun method name arg = Future.join (promise_method name arg); diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/System/isabelle_process.ML Mon Mar 31 10:28:08 2014 +0200 @@ -106,7 +106,7 @@ Message_Channel.send msg_channel (Message_Channel.message name props body); fun standard_message props name body = - if body = "" then () + if forall (fn s => s = "") body then () else message name (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body; @@ -124,7 +124,7 @@ Output.protocol_message_fn := message Markup.protocolN; Output.urgent_message_fn := ! Output.writeln_fn; Output.prompt_fn := ignore; - message Markup.initN [] (Session.welcome ()); + message Markup.initN [] [Session.welcome ()]; msg_channel end; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/System/message_channel.ML Mon Mar 31 10:28:08 2014 +0200 @@ -7,7 +7,7 @@ signature MESSAGE_CHANNEL = sig type message - val message: string -> Properties.T -> string -> message + val message: string -> Properties.T -> string list -> message type T val send: T -> message -> unit val shutdown: T -> unit @@ -21,13 +21,14 @@ datatype message = Message of string list; -fun chunk s = [string_of_int (size s), "\n", s]; +fun chunk ss = + string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss; fun message name raw_props body = let val robust_props = map (pairself YXML.embed_controls) raw_props; val header = YXML.string_of (XML.Elem ((name, robust_props), [])); - in Message (chunk header @ chunk body) end; + in Message (chunk [header] @ chunk body) end; fun output_message channel (Message ss) = List.app (System_Channel.output channel) ss; @@ -37,7 +38,7 @@ fun flush channel = ignore (try System_Channel.flush channel); -val flush_message = message Markup.protocolN Markup.flush ""; +val flush_message = message Markup.protocolN Markup.flush []; fun flush_output channel = (output_message channel flush_message; flush channel); diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Mar 31 10:28:08 2014 +0200 @@ -269,7 +269,7 @@ let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); - val _ = Output.try_protocol_message (Markup.loading_theory name) ""; + val _ = Output.try_protocol_message (Markup.loading_theory name) []; val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Tools/proof_general.ML Mon Mar 31 10:28:08 2014 +0200 @@ -258,8 +258,8 @@ (* hooks *) -fun message bg en prfx text = - (case render text of +fun message bg en prfx body = + (case render (implode body) of "" => () | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s))); @@ -276,7 +276,7 @@ (* notification *) -val emacs_notify = message (special "I") (special "J") ""; +fun emacs_notify s = message (special "I") (special "J") "" [s]; fun tell_clear_goals () = emacs_notify "Proof General, please clear the goals buffer."; diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Tools/simplifier_trace.ML Mon Mar 31 10:28:08 2014 +0200 @@ -133,7 +133,7 @@ (** markup **) fun output_result (id, data) = - Output.result (Markup.serial_properties id) data + Output.result (Markup.serial_properties id) [data] val parentN = "parent" val textN = "text" @@ -184,7 +184,7 @@ fun send_request (result_id, content) = let fun break () = - (Output.protocol_message (Markup.simp_trace_cancel result_id) ""; + (Output.protocol_message (Markup.simp_trace_cancel result_id) []; Synchronized.change futures (Inttab.delete_safe result_id)) val promise = Future.promise break : string future in diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/context_position.ML Mon Mar 31 10:28:08 2014 +0200 @@ -49,13 +49,13 @@ fun report_generic context pos markup = if is_reported_generic context pos then - Output.report (Position.reported_text pos markup "") + Output.report [Position.reported_text pos markup ""] else (); fun reported_text ctxt pos markup txt = if is_reported ctxt pos then Position.reported_text pos markup txt else ""; -fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); +fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt]; fun report ctxt pos markup = report_text ctxt pos markup ""; fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else (); diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/skip_proof.ML --- a/src/Pure/skip_proof.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/skip_proof.ML Mon Mar 31 10:28:08 2014 +0200 @@ -19,7 +19,7 @@ fun report ctxt = if Context_Position.is_visible ctxt then - Output.report (Markup.markup Markup.bad "Skipped proof") + Output.report [Markup.markup Markup.bad "Skipped proof"] else ();