added transform_error, exception ERROR_MESSAGE;
authorwenzelm
Wed May 13 19:05:50 1998 +0200 (1998-05-13)
changeset 4923ec71c480e600
parent 4922 03b81b6e1baa
child 4924 cf6bb75968c4
added transform_error, exception ERROR_MESSAGE;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed May 13 12:23:28 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Wed May 13 19:05:50 1998 +0200
     1.3 @@ -215,6 +215,8 @@
     1.4    val get_error: 'a error -> string option
     1.5    val get_ok: 'a error -> 'a option
     1.6    val handle_error: ('a -> 'b) -> 'a -> 'b error
     1.7 +  exception ERROR_MESSAGE of string
     1.8 +  val transform_error: ('a -> 'b) -> 'a -> 'b
     1.9  
    1.10    (*timing*)
    1.11    val cond_timeit: bool -> (unit -> 'a) -> 'a
    1.12 @@ -1061,6 +1063,16 @@
    1.13    end;
    1.14  
    1.15  
    1.16 +(* transform ERROR into ERROR_MESSAGE, capturing the side-effect *)
    1.17 +
    1.18 +exception ERROR_MESSAGE of string;
    1.19 +
    1.20 +fun transform_error f x =
    1.21 +  (case handle_error f x of
    1.22 +    OK y => y
    1.23 +  | Error msg => raise ERROR_MESSAGE msg);
    1.24 +
    1.25 +
    1.26  
    1.27  (** timing **)
    1.28