priority_fn := decorate_lines;
authorwenzelm
Fri Sep 01 00:32:46 2000 +0200 (2000-09-01)
changeset 9775da698a96c4f3
parent 9774 e745a418e6a5
child 9776 a126bc3b7376
priority_fn := decorate_lines;
replaced 'message' by 'priority';
src/Pure/Interface/proof_general.ML
     1.1 --- a/src/Pure/Interface/proof_general.ML	Fri Sep 01 00:32:11 2000 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Fri Sep 01 00:32:46 2000 +0200
     1.3 @@ -90,18 +90,17 @@
     1.4  fun decorate_lines bg en "" = plain_output o enclose bg en
     1.5    | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
     1.6  
     1.7 -val message = decorate_lines (oct_char "360") (oct_char "361") "";
     1.8 -
     1.9  fun setup_messages () =
    1.10 - (warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
    1.11 + (priority_fn := decorate_lines (oct_char "360") (oct_char "361") "";
    1.12 +  warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
    1.13    error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
    1.14  
    1.15  
    1.16  (* notification *)
    1.17  
    1.18 -fun tell_clear_goals () = message "Proof General, please clear the goals buffer.";
    1.19 -fun tell_clear_response () = message "Proof General, please clear the response buffer.";
    1.20 -fun tell_file msg path = message ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
    1.21 +fun tell_clear_goals () = priority "Proof General, please clear the goals buffer.";
    1.22 +fun tell_clear_response () = priority "Proof General, please clear the response buffer.";
    1.23 +fun tell_file msg path = priority ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
    1.24  
    1.25  
    1.26  (* theory / proof state output *)
    1.27 @@ -168,7 +167,7 @@
    1.28  
    1.29  fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
    1.30  
    1.31 -val welcome = message o Session.welcome;
    1.32 +val welcome = priority o Session.welcome;
    1.33  val help = welcome;
    1.34  val show_context = Context.the_context;
    1.35