src/Pure/General/output.ML
changeset 44270 3eaad39e520c
parent 43760 ef8375a4dae4
child 44389 a3b5fdfb04a3
     1.1 --- a/src/Pure/General/output.ML	Thu Aug 18 17:30:47 2011 +0200
     1.2 +++ b/src/Pure/General/output.ML	Thu Aug 18 17:53:32 2011 +0200
     1.3 @@ -31,13 +31,14 @@
     1.4      val urgent_message_fn: (output -> unit) Unsynchronized.ref
     1.5      val tracing_fn: (output -> unit) Unsynchronized.ref
     1.6      val warning_fn: (output -> unit) Unsynchronized.ref
     1.7 -    val error_fn: (output -> unit) Unsynchronized.ref
     1.8 +    val error_fn: (serial * output -> unit) Unsynchronized.ref
     1.9      val prompt_fn: (output -> unit) Unsynchronized.ref
    1.10      val status_fn: (output -> unit) Unsynchronized.ref
    1.11      val report_fn: (output -> unit) Unsynchronized.ref
    1.12      val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    1.13    end
    1.14    val urgent_message: string -> unit
    1.15 +  val error_msg': serial * string -> unit
    1.16    val error_msg: string -> unit
    1.17    val prompt: string -> unit
    1.18    val status: string -> unit
    1.19 @@ -92,7 +93,8 @@
    1.20    val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.21    val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.22    val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    1.23 -  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    1.24 +  val error_fn =
    1.25 +    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
    1.26    val prompt_fn = Unsynchronized.ref raw_stdout;
    1.27    val status_fn = Unsynchronized.ref (fn _: output => ());
    1.28    val report_fn = Unsynchronized.ref (fn _: output => ());
    1.29 @@ -104,7 +106,8 @@
    1.30  fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
    1.31  fun tracing s = ! Private_Hooks.tracing_fn (output s);
    1.32  fun warning s = ! Private_Hooks.warning_fn (output s);
    1.33 -fun error_msg s = ! Private_Hooks.error_fn (output s);
    1.34 +fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
    1.35 +fun error_msg s = error_msg' (serial (), s);
    1.36  fun prompt s = ! Private_Hooks.prompt_fn (output s);
    1.37  fun status s = ! Private_Hooks.status_fn (output s);
    1.38  fun report s = ! Private_Hooks.report_fn (output s);