# HG changeset patch
# User wenzelm
# Date 967761131 -7200
# Node ID e745a418e6a5b8bf6a288ac8c5e50db255378083
# Parent  c5024f705d2492983a5eac7701f151a9af771ad7
added priority, priority_fn;

diff -r c5024f705d24 -r e745a418e6a5 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Sep 01 00:31:39 2000 +0200
+++ b/src/Pure/library.ML	Fri Sep 01 00:32:11 2000 +0200
@@ -223,9 +223,11 @@
   val cd: string -> unit
   val pwd: unit -> string
   val writeln_fn: (string -> unit) ref
+  val priority_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 warning: string -> unit
   exception ERROR
   val error_msg: string -> unit
@@ -1113,10 +1115,12 @@
 
 (*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 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 warning s = ! warning_fn s;
 
 (*print error message and abort to top level*)