# HG changeset patch
# User wenzelm
# Date 967761166 -7200
# Node ID da698a96c4f32408b1266c95010981ed4449d262
# Parent  e745a418e6a5b8bf6a288ac8c5e50db255378083
priority_fn := decorate_lines;
replaced 'message' by 'priority';

diff -r e745a418e6a5 -r da698a96c4f3 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Fri Sep 01 00:32:11 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Fri Sep 01 00:32:46 2000 +0200
@@ -90,18 +90,17 @@
 fun decorate_lines bg en "" = plain_output o enclose bg en
   | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
 
-val message = decorate_lines (oct_char "360") (oct_char "361") "";
-
 fun setup_messages () =
- (warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
+ (priority_fn := decorate_lines (oct_char "360") (oct_char "361") "";
+  warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
   error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
 
 
 (* notification *)
 
-fun tell_clear_goals () = message "Proof General, please clear the goals buffer.";
-fun tell_clear_response () = message "Proof General, please clear the response buffer.";
-fun tell_file msg path = message ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
+fun tell_clear_goals () = priority "Proof General, please clear the goals buffer.";
+fun tell_clear_response () = priority "Proof General, please clear the response buffer.";
+fun tell_file msg path = priority ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
 
 
 (* theory / proof state output *)
@@ -168,7 +167,7 @@
 
 fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
 
-val welcome = message o Session.welcome;
+val welcome = priority o Session.welcome;
 val help = welcome;
 val show_context = Context.the_context;