src/Pure/General/output.ML
changeset 58843 521cea5fa777
parent 57975 c657c68a60ab
child 58850 1bb0ad7827b4
     1.1 --- a/src/Pure/General/output.ML	Fri Oct 31 11:18:17 2014 +0100
     1.2 +++ b/src/Pure/General/output.ML	Fri Oct 31 11:36:41 2014 +0100
     1.3 @@ -26,7 +26,6 @@
     1.4    val physical_writeln: output -> unit
     1.5    exception Protocol_Message of Properties.T
     1.6    val writelns: string list -> unit
     1.7 -  val urgent_message: string -> unit
     1.8    val error_message': serial * string -> unit
     1.9    val error_message: string -> unit
    1.10    val system_message: string -> unit
    1.11 @@ -42,7 +41,6 @@
    1.12  sig
    1.13    include OUTPUT
    1.14    val writeln_fn: (output list -> unit) Unsynchronized.ref
    1.15 -  val urgent_message_fn: (output list -> unit) Unsynchronized.ref
    1.16    val tracing_fn: (output list -> unit) Unsynchronized.ref
    1.17    val warning_fn: (output list -> unit) Unsynchronized.ref
    1.18    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    1.19 @@ -98,7 +96,6 @@
    1.20  exception Protocol_Message of Properties.T;
    1.21  
    1.22  val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
    1.23 -val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);  (*Proof General legacy*)
    1.24  val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.25  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    1.26  val error_message_fn =
    1.27 @@ -113,7 +110,6 @@
    1.28  
    1.29  fun writelns ss = ! writeln_fn (map output ss);
    1.30  fun writeln s = writelns [s];
    1.31 -fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
    1.32  fun tracing s = ! tracing_fn [output s];
    1.33  fun warning s = ! warning_fn [output s];
    1.34  fun error_message' (i, s) = ! error_message_fn (i, [output s]);