src/Pure/library.ML
changeset 4792 8e3c2dddb9c8
parent 4713 bea2ab2e360b
child 4849 a9d5b8f8e40f
     1.1 --- a/src/Pure/library.ML	Sat Apr 04 11:44:16 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Apr 04 12:26:47 1998 +0200
     1.3 @@ -234,6 +234,7 @@
     1.4    val scanwords: (string -> bool) -> string list -> string list
     1.5    datatype 'a mtree = Join of 'a * 'a mtree list
     1.6    type object
     1.7 +  val type_error: string -> 'a
     1.8  end;
     1.9  
    1.10  structure Library: LIBRARY =
    1.11 @@ -1004,7 +1005,7 @@
    1.12  exception ERROR;
    1.13  fun error_msg s = !error_fn s;	  (*promise to raise ERROR later!*)
    1.14  fun error s = (error_msg s; raise ERROR);
    1.15 -fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);
    1.16 +fun sys_error msg = error ("!! SYSTEM ERROR !!\n" ^ msg);
    1.17  
    1.18  fun assert p msg = if p then () else error msg;
    1.19  fun deny p msg = if p then error msg else ();
    1.20 @@ -1206,8 +1207,12 @@
    1.21  
    1.22  
    1.23  (* generic objects -- fool the ML type system via exception constructors *)
    1.24 +
    1.25  type object = exn;
    1.26  
    1.27 +fun type_error name =
    1.28 +  error ("!! RUNTIME TYPE ERROR !!\nFailed to access " ^ quote name ^ " data");
    1.29 +
    1.30  
    1.31  end;
    1.32