1.1 --- a/src/Pure/System/isabelle_process.ML	Mon Oct 01 20:16:37 2012 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Oct 01 20:17:30 2012 +0200
     1.3 @@ -89,16 +89,16 @@
     1.4  
     1.5  fun chunk s = [string_of_int (size s), "\n", s];
     1.6  
     1.7 -fun message do_flush mbox ch raw_props body =
     1.8 +fun message do_flush mbox name raw_props body =
     1.9    let
    1.10      val robust_props = map (pairself YXML.embed_controls) raw_props;
    1.11 -    val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    1.12 +    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
    1.13    in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
    1.14  
    1.15 -fun standard_message mbox opt_serial ch body =
    1.16 +fun standard_message mbox opt_serial name body =
    1.17    if body = "" then ()
    1.18    else
    1.19 -    message false mbox ch
    1.20 +    message false mbox name
    1.21        ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
    1.22          (Position.properties_of (Position.thread_data ()))) body;
    1.23  
    1.24 @@ -124,17 +124,22 @@
    1.25      val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    1.26      val _ = Simple_Thread.fork false (message_output mbox channel);
    1.27    in
    1.28 -    Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    1.29 -    Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    1.30 -    Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
    1.31 +    Output.Private_Hooks.status_fn := standard_message mbox NONE Isabelle_Markup.statusN;
    1.32 +    Output.Private_Hooks.report_fn := standard_message mbox NONE Isabelle_Markup.reportN;
    1.33 +    Output.Private_Hooks.writeln_fn :=
    1.34 +      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.writelnN s);
    1.35      Output.Private_Hooks.tracing_fn :=
    1.36 -      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
    1.37 -    Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    1.38 -    Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    1.39 -    Output.Private_Hooks.protocol_message_fn := message true mbox "H";
    1.40 +      (fn s =>
    1.41 +        (update_tracing_limits s;
    1.42 +          standard_message mbox (SOME (serial ())) Isabelle_Markup.tracingN s));
    1.43 +    Output.Private_Hooks.warning_fn :=
    1.44 +      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.warningN s);
    1.45 +    Output.Private_Hooks.error_fn :=
    1.46 +      (fn (i, s) => standard_message mbox (SOME i) Isabelle_Markup.errorN s);
    1.47 +    Output.Private_Hooks.protocol_message_fn := message true mbox Isabelle_Markup.protocolN;
    1.48      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.49      Output.Private_Hooks.prompt_fn := ignore;
    1.50 -    message true mbox "A" [] (Session.welcome ())
    1.51 +    message true mbox Isabelle_Markup.initN [] (Session.welcome ())
    1.52    end;
    1.53  
    1.54  end;