--- a/src/Pure/General/output.ML Fri Oct 31 11:18:17 2014 +0100
+++ b/src/Pure/General/output.ML Fri Oct 31 11:36:41 2014 +0100
@@ -26,7 +26,6 @@
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
val writelns: string list -> unit
- val urgent_message: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
val system_message: string -> unit
@@ -42,7 +41,6 @@
sig
include OUTPUT
val writeln_fn: (output list -> unit) Unsynchronized.ref
- val urgent_message_fn: (output list -> unit) Unsynchronized.ref
val tracing_fn: (output list -> unit) Unsynchronized.ref
val warning_fn: (output list -> unit) Unsynchronized.ref
val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
@@ -98,7 +96,6 @@
exception Protocol_Message of Properties.T;
val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
-val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*)
val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
@@ -113,7 +110,6 @@
fun writelns ss = ! writeln_fn (map output ss);
fun writeln s = writelns [s];
-fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*)
fun tracing s = ! tracing_fn [output s];
fun warning s = ! warning_fn [output s];
fun error_message' (i, s) = ! error_message_fn (i, [output s]);