1.1 --- a/src/Pure/General/output.ML	Tue Jun 01 15:02:05 2004 +0200
     1.2 +++ b/src/Pure/General/output.ML	Tue Jun 01 18:51:55 2004 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val tracing_fn: (string -> unit) ref
     1.5    val warning_fn: (string -> unit) ref
     1.6    val error_fn: (string -> unit) ref
     1.7 +  val panic_fn: (string -> unit) ref
     1.8    val writeln: string -> unit
     1.9    val priority: string -> unit
    1.10    val tracing: string -> unit
    1.11 @@ -24,6 +25,7 @@
    1.12    val error_msg: string -> unit
    1.13    val error: string -> 'a
    1.14    val sys_error: string -> 'a
    1.15 +  val panic: string -> unit
    1.16    val assert: bool -> string -> unit
    1.17    val deny: bool -> string -> unit
    1.18    val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    1.19 @@ -99,13 +101,14 @@
    1.20  val tracing_fn = ref (fn s => ! writeln_fn s);
    1.21  val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
    1.22  val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
    1.23 +val panic_fn = ref (std_output o suffix "\n" o prefix_lines "!!! ");
    1.24  
    1.25  fun writeln s = ! writeln_fn (output s);
    1.26  fun priority s = ! priority_fn (output s);
    1.27  fun tracing s = ! tracing_fn (output s);
    1.28  fun warning s = ! warning_fn (output s);
    1.29  fun error_msg s = ! error_fn (output s);
    1.30 -
    1.31 +fun panic_msg s = ! panic_fn (output s);
    1.32  
    1.33  (* add_mode *)
    1.34  
    1.35 @@ -115,10 +118,11 @@
    1.36    modes := Symtab.update ((name, m), ! modes));
    1.37  
    1.38  
    1.39 -(* error/warning forms *)
    1.40 +(* output error message and abort to top level, or panic & exit *)
    1.41  
    1.42  fun error s = (error_msg s; raise ERROR);
    1.43  fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
    1.44 +fun panic s = (panic_msg ("## SYSTEM EXIT ##\n" ^ s); exit 1);
    1.45  
    1.46  fun assert p msg = if p then () else error msg;
    1.47  fun deny p msg = if p then error msg else ();