tuned error msgs;
authorwenzelm
Wed Apr 29 11:22:52 1998 +0200 (1998-04-29)
changeset 4849a9d5b8f8e40f
parent 4848 99c8d95c51d6
child 4850 050481f41e28
tuned error msgs;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Apr 29 11:22:01 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Apr 29 11:22:52 1998 +0200
     1.3 @@ -1005,7 +1005,7 @@
     1.4  exception ERROR;
     1.5  fun error_msg s = !error_fn s;	  (*promise to raise ERROR later!*)
     1.6  fun error s = (error_msg s; raise ERROR);
     1.7 -fun sys_error msg = error ("!! SYSTEM ERROR !!\n" ^ msg);
     1.8 +fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
     1.9  
    1.10  fun assert p msg = if p then () else error msg;
    1.11  fun deny p msg = if p then error msg else ();
    1.12 @@ -1211,7 +1211,7 @@
    1.13  type object = exn;
    1.14  
    1.15  fun type_error name =
    1.16 -  error ("!! RUNTIME TYPE ERROR !!\nFailed to access " ^ quote name ^ " data");
    1.17 +  error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote name ^ " data");
    1.18  
    1.19  
    1.20  end;