# HG changeset patch
# User wenzelm
# Date 1006299278 -3600
# Node ID 4898247d0102c861c842fb22610863aeb762f2ae
# Parent  3949e7aba298108476315fbc86b2740b8f2f6106
added tracing, tracing_fn;

diff -r 3949e7aba298 -r 4898247d0102 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Nov 21 00:34:06 2001 +0100
+++ b/src/Pure/library.ML	Wed Nov 21 00:34:38 2001 +0100
@@ -245,10 +245,12 @@
   val pwd: unit -> string
   val writeln_fn: (string -> unit) ref
   val priority_fn: (string -> unit) ref
+  val tracing_fn: (string -> unit) ref
   val warning_fn: (string -> unit) ref
   val error_fn: (string -> unit) ref
   val writeln: string -> unit
   val priority: string -> unit
+  val tracing: string -> unit
   val warning: string -> unit
   exception ERROR
   val error_msg: string -> unit
@@ -1174,11 +1176,13 @@
 (*hooks for output channels: normal, warning, error*)
 val writeln_fn = ref (std_output o suffix "\n");
 val priority_fn = ref (fn s => ! writeln_fn s);
+val tracing_fn = ref (fn s => ! writeln_fn s);
 val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
 val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
 
 fun writeln s = ! writeln_fn s;
 fun priority s = ! priority_fn s;
+fun tracing s = ! tracing_fn s;
 fun warning s = ! warning_fn s;
 
 (*print error message and abort to top level*)