src/Pure/System/isabelle_process.ML
changeset 52854 92932931bd82
parent 52852 08ecbffaf25c
child 53192 04df1d236e1c
     1.1 --- a/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:13:31 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Aug 02 22:17:53 2013 +0200
     1.3 @@ -93,6 +93,8 @@
     1.4  
     1.5  (* output channels *)
     1.6  
     1.7 +val serial_props = Markup.serial_properties o serial;
     1.8 +
     1.9  fun init_channels channel =
    1.10    let
    1.11      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.12 @@ -103,21 +105,22 @@
    1.13      fun message name props body =
    1.14        Message_Channel.send msg_channel (Message_Channel.message name props body);
    1.15  
    1.16 -    fun standard_message opt_serial name body =
    1.17 +    fun standard_message props name body =
    1.18        if body = "" then ()
    1.19        else
    1.20          message name
    1.21 -          ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
    1.22 -            (Position.properties_of (Position.thread_data ()))) body;
    1.23 +          (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
    1.24    in
    1.25 -    Output.Internal.status_fn := standard_message NONE Markup.statusN;
    1.26 -    Output.Internal.report_fn := standard_message NONE Markup.reportN;
    1.27 -    Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
    1.28 -    Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
    1.29 +    Output.Internal.status_fn := standard_message [] Markup.statusN;
    1.30 +    Output.Internal.report_fn := standard_message [] Markup.reportN;
    1.31 +    Output.Internal.result_fn :=
    1.32 +      (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
    1.33 +    Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    1.34      Output.Internal.tracing_fn :=
    1.35 -      (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
    1.36 -    Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    1.37 -    Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    1.38 +      (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
    1.39 +    Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    1.40 +    Output.Internal.error_fn :=
    1.41 +      (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    1.42      Output.Internal.protocol_message_fn := message Markup.protocolN;
    1.43      Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
    1.44      Output.Internal.prompt_fn := ignore;