# HG changeset patch
# User wenzelm
# Date 895079150 -7200
# Node ID ec71c480e600900a3031e013c6a42bd38dda060c
# Parent  03b81b6e1baa8185bf3cfd4b5b40035679fad297
added transform_error, exception ERROR_MESSAGE;

diff -r 03b81b6e1baa -r ec71c480e600 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed May 13 12:23:28 1998 +0200
+++ b/src/Pure/library.ML	Wed May 13 19:05:50 1998 +0200
@@ -215,6 +215,8 @@
   val get_error: 'a error -> string option
   val get_ok: 'a error -> 'a option
   val handle_error: ('a -> 'b) -> 'a -> 'b error
+  exception ERROR_MESSAGE of string
+  val transform_error: ('a -> 'b) -> 'a -> 'b
 
   (*timing*)
   val cond_timeit: bool -> (unit -> 'a) -> 'a
@@ -1061,6 +1063,16 @@
   end;
 
 
+(* transform ERROR into ERROR_MESSAGE, capturing the side-effect *)
+
+exception ERROR_MESSAGE of string;
+
+fun transform_error f x =
+  (case handle_error f x of
+    OK y => y
+  | Error msg => raise ERROR_MESSAGE msg);
+
+
 
 (** timing **)