1.1 --- a/src/Pure/System/isabelle_process.ML	Sun Nov 25 18:50:13 2012 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Sun Nov 25 19:49:24 2012 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4    if body = "" then ()
     1.5    else
     1.6      message false mbox name
     1.7 -      ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
     1.8 +      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
     1.9          (Position.properties_of (Position.thread_data ()))) body;
    1.10  
    1.11  fun message_output mbox channel =
    1.12 @@ -124,22 +124,20 @@
    1.13      val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    1.14      val _ = Simple_Thread.fork false (message_output mbox channel);
    1.15    in
    1.16 -    Output.Private_Hooks.status_fn := standard_message mbox NONE Isabelle_Markup.statusN;
    1.17 -    Output.Private_Hooks.report_fn := standard_message mbox NONE Isabelle_Markup.reportN;
    1.18 +    Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
    1.19 +    Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
    1.20      Output.Private_Hooks.writeln_fn :=
    1.21 -      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.writelnN s);
    1.22 +      (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
    1.23      Output.Private_Hooks.tracing_fn :=
    1.24 -      (fn s =>
    1.25 -        (update_tracing_limits s;
    1.26 -          standard_message mbox (SOME (serial ())) Isabelle_Markup.tracingN s));
    1.27 +      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
    1.28      Output.Private_Hooks.warning_fn :=
    1.29 -      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.warningN s);
    1.30 +      (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
    1.31      Output.Private_Hooks.error_fn :=
    1.32 -      (fn (i, s) => standard_message mbox (SOME i) Isabelle_Markup.errorN s);
    1.33 -    Output.Private_Hooks.protocol_message_fn := message true mbox Isabelle_Markup.protocolN;
    1.34 +      (fn (i, s) => standard_message mbox (SOME i) Markup.errorN s);
    1.35 +    Output.Private_Hooks.protocol_message_fn := message true mbox Markup.protocolN;
    1.36      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.37      Output.Private_Hooks.prompt_fn := ignore;
    1.38 -    message true mbox Isabelle_Markup.initN [] (Session.welcome ())
    1.39 +    message true mbox Markup.initN [] (Session.welcome ())
    1.40    end;
    1.41  
    1.42  end;