src/Pure/General/output.ML
changeset 57975 c657c68a60ab
parent 56830 e760242101fc
child 58843 521cea5fa777
     1.1 --- a/src/Pure/General/output.ML	Wed Aug 13 20:21:04 2014 +0200
     1.2 +++ b/src/Pure/General/output.ML	Fri Aug 15 13:39:59 2014 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val urgent_message: string -> unit
     1.5    val error_message': serial * string -> unit
     1.6    val error_message: string -> unit
     1.7 +  val system_message: string -> unit
     1.8    val prompt: string -> unit
     1.9    val status: string -> unit
    1.10    val report: string list -> unit
    1.11 @@ -45,6 +46,7 @@
    1.12    val tracing_fn: (output list -> unit) Unsynchronized.ref
    1.13    val warning_fn: (output list -> unit) Unsynchronized.ref
    1.14    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    1.15 +  val system_message_fn: (output list -> unit) Unsynchronized.ref
    1.16    val prompt_fn: (output -> unit) Unsynchronized.ref
    1.17    val status_fn: (output list -> unit) Unsynchronized.ref
    1.18    val report_fn: (output list -> unit) Unsynchronized.ref
    1.19 @@ -101,6 +103,7 @@
    1.20  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    1.21  val error_message_fn =
    1.22    Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.23 +val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.24  val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
    1.25  val status_fn = Unsynchronized.ref (fn _: output list => ());
    1.26  val report_fn = Unsynchronized.ref (fn _: output list => ());
    1.27 @@ -115,6 +118,7 @@
    1.28  fun warning s = ! warning_fn [output s];
    1.29  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    1.30  fun error_message s = error_message' (serial (), s);
    1.31 +fun system_message s = ! system_message_fn [output s];
    1.32  fun prompt s = ! prompt_fn (output s);
    1.33  fun status s = ! status_fn [output s];
    1.34  fun report ss = ! report_fn (map output ss);