src/Pure/System/isabelle_process.ML
changeset 44270 3eaad39e520c
parent 43772 c825594fd0c1
child 44389 a3b5fdfb04a3
     1.1 --- a/src/Pure/System/isabelle_process.ML	Thu Aug 18 17:30:47 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Aug 18 17:53:32 2011 +0200
     1.3 @@ -72,11 +72,11 @@
     1.4      val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
     1.5    in Mailbox.send mbox (chunk header @ chunk body) end;
     1.6  
     1.7 -fun standard_message mbox with_serial ch body =
     1.8 +fun standard_message mbox opt_serial ch body =
     1.9    if body = "" then ()
    1.10    else
    1.11      message mbox ch
    1.12 -      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
    1.13 +      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    1.14          (Position.properties_of (Position.thread_data ()))) body;
    1.15  
    1.16  fun message_output mbox out_stream =
    1.17 @@ -103,12 +103,12 @@
    1.18      val mbox = Mailbox.create () : string list Mailbox.T;
    1.19      val _ = Simple_Thread.fork false (message_output mbox out_stream);
    1.20    in
    1.21 -    Output.Private_Hooks.status_fn := standard_message mbox false "B";
    1.22 -    Output.Private_Hooks.report_fn := standard_message mbox false "C";
    1.23 -    Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
    1.24 -    Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
    1.25 -    Output.Private_Hooks.warning_fn := standard_message mbox true "F";
    1.26 -    Output.Private_Hooks.error_fn := standard_message mbox true "G";
    1.27 +    Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    1.28 +    Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    1.29 +    Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
    1.30 +    Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
    1.31 +    Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    1.32 +    Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    1.33      Output.Private_Hooks.raw_message_fn := message mbox "H";
    1.34      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.35      Output.Private_Hooks.prompt_fn := ignore;