1.1 --- a/src/Pure/System/isabelle_process.ML Fri Aug 02 16:02:06 2013 +0200
1.2 +++ b/src/Pure/System/isabelle_process.ML Fri Aug 02 20:47:02 2013 +0200
1.3 @@ -110,20 +110,17 @@
1.4 ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
1.5 (Position.properties_of (Position.thread_data ()))) body;
1.6 in
1.7 - Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
1.8 - Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
1.9 - Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
1.10 - Output.Private_Hooks.writeln_fn :=
1.11 - (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
1.12 - Output.Private_Hooks.tracing_fn :=
1.13 + Output.Internal.status_fn := standard_message NONE Markup.statusN;
1.14 + Output.Internal.report_fn := standard_message NONE Markup.reportN;
1.15 + Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
1.16 + Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
1.17 + Output.Internal.tracing_fn :=
1.18 (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
1.19 - Output.Private_Hooks.warning_fn :=
1.20 - (fn s => standard_message (SOME (serial ())) Markup.warningN s);
1.21 - Output.Private_Hooks.error_fn :=
1.22 - (fn (i, s) => standard_message (SOME i) Markup.errorN s);
1.23 - Output.Private_Hooks.protocol_message_fn := message Markup.protocolN;
1.24 - Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
1.25 - Output.Private_Hooks.prompt_fn := ignore;
1.26 + Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s);
1.27 + Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s);
1.28 + Output.Internal.protocol_message_fn := message Markup.protocolN;
1.29 + Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
1.30 + Output.Internal.prompt_fn := ignore;
1.31 message Markup.initN [] (Session.welcome ());
1.32 msg_channel
1.33 end;