# HG changeset patch
# User wenzelm
# Date 875028907 -7200
# Node ID 7c30ab9e25d15894f05cf15ceac8385dc637f23c
# Parent  0b8986fd9bfccaa3c967e53de9a0428d96c148d4
added handle_error: ('a -> 'b) -> 'a -> 'b error;

diff -r 0b8986fd9bfc -r 7c30ab9e25d1 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Sep 23 08:44:57 1997 +0200
+++ b/src/Pure/library.ML	Tue Sep 23 17:35:07 1997 +0200
@@ -771,6 +771,24 @@
   in  asl l  end;
 
 
+(* handle errors (capturing messages) *)
+
+datatype 'a error =
+  Error of string |
+  OK of 'a;
+
+fun handle_error f x =
+  let
+    val buffer = ref "";
+    fun capture s = buffer := ! buffer ^ s ^ "\n";
+    val result = Some (setmp error_fn capture f x) handle ERROR => None;
+  in
+    case result of
+      None => Error (! buffer)
+    | Some y => OK y
+  end;
+
+
 (* read / write files *)
 
 fun read_file name =