src/Pure/library.ML
changeset 19542 b5abe6cd4cbf
parent 19512 94cd541dc8fa
child 19567 48d3b4266b52
     1.1 --- a/src/Pure/library.ML	Tue May 02 20:42:37 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Tue May 02 20:42:37 2006 +0200
     1.3 @@ -67,10 +67,11 @@
     1.4    val get_exn: 'a result -> exn option
     1.5  
     1.6    (*errors*)
     1.7 +  exception SYS_ERROR of string
     1.8 +  val sys_error: string -> 'a
     1.9    exception ERROR of string
    1.10    val error: string -> 'a
    1.11    val cat_error: string -> string -> 'a
    1.12 -  val sys_error: string -> 'a
    1.13    val assert: bool -> string -> unit
    1.14    val deny: bool -> string -> unit
    1.15    val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    1.16 @@ -405,15 +406,15 @@
    1.17  
    1.18  (* errors *)
    1.19  
    1.20 +exception SYS_ERROR of string;
    1.21 +fun sys_error msg = raise SYS_ERROR msg;
    1.22 +
    1.23  exception ERROR of string;
    1.24 -
    1.25  fun error msg = raise ERROR msg;
    1.26  
    1.27  fun cat_error "" msg = error msg
    1.28    | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
    1.29  
    1.30 -fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
    1.31 -
    1.32  fun assert p msg = if p then () else error msg;
    1.33  fun deny p msg = if p then error msg else ();
    1.34