discontinued obsolete function sys_error and exception SYS_ERROR;
authorwenzelm
Wed Nov 03 11:33:51 2010 +0100 (2010-11-03)
changeset 40318035b2afbeb2e
parent 40317 1eac228c52b3
child 40319 daaa0b236a3f
discontinued obsolete function sys_error and exception SYS_ERROR;
NEWS
src/Pure/Isar/runtime.ML
src/Pure/library.ML
     1.1 --- a/NEWS	Wed Nov 03 11:11:49 2010 +0100
     1.2 +++ b/NEWS	Wed Nov 03 11:33:51 2010 +0100
     1.3 @@ -349,6 +349,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Discontinued obsolete function sys_error and exception SYS_ERROR.
     1.8 +See implementation manual for further details on exceptions in
     1.9 +Isabelle/ML.
    1.10 +
    1.11  * Antiquotation @{assert} inlines a function bool -> unit that raises
    1.12  Fail if the argument is false.  Due to inlining the source position of
    1.13  failed assertions is included in the error output.
     2.1 --- a/src/Pure/Isar/runtime.ML	Wed Nov 03 11:11:49 2010 +0100
     2.2 +++ b/src/Pure/Isar/runtime.ML	Wed Nov 03 11:33:51 2010 +0100
     2.3 @@ -68,7 +68,6 @@
     2.4          | TERMINATE => ["Exit"]
     2.5          | TimeLimit.TimeOut => ["Timeout"]
     2.6          | TOPLEVEL_ERROR => ["Error"]
     2.7 -        | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
     2.8          | ERROR msg => [msg]
     2.9          | Fail msg => [raised exn "Fail" [msg]]
    2.10          | THEORY (msg, thys) =>
     3.1 --- a/src/Pure/library.ML	Wed Nov 03 11:11:49 2010 +0100
     3.2 +++ b/src/Pure/library.ML	Wed Nov 03 11:33:51 2010 +0100
     3.3 @@ -29,8 +29,6 @@
     3.4    val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
     3.5  
     3.6    (*errors*)
     3.7 -  exception SYS_ERROR of string
     3.8 -  val sys_error: string -> 'a
     3.9    exception ERROR of string
    3.10    val error: string -> 'a
    3.11    val cat_error: string -> string -> 'a
    3.12 @@ -256,11 +254,9 @@
    3.13  fun funpow_yield (0 : int) _ x = ([], x)
    3.14    | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
    3.15  
    3.16 +
    3.17  (* errors *)
    3.18  
    3.19 -exception SYS_ERROR of string;
    3.20 -fun sys_error msg = raise SYS_ERROR msg;
    3.21 -
    3.22  exception ERROR of string;
    3.23  fun error msg = raise ERROR msg;
    3.24