added handle_error: ('a -> 'b) -> 'a -> 'b error;
authorwenzelm
Tue Sep 23 17:35:07 1997 +0200 (1997-09-23)
changeset 36997c30ab9e25d1
parent 3698 0b8986fd9bfc
child 3700 3a8192e83579
added handle_error: ('a -> 'b) -> 'a -> 'b error;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Sep 23 08:44:57 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Sep 23 17:35:07 1997 +0200
     1.3 @@ -771,6 +771,24 @@
     1.4    in  asl l  end;
     1.5  
     1.6  
     1.7 +(* handle errors (capturing messages) *)
     1.8 +
     1.9 +datatype 'a error =
    1.10 +  Error of string |
    1.11 +  OK of 'a;
    1.12 +
    1.13 +fun handle_error f x =
    1.14 +  let
    1.15 +    val buffer = ref "";
    1.16 +    fun capture s = buffer := ! buffer ^ s ^ "\n";
    1.17 +    val result = Some (setmp error_fn capture f x) handle ERROR => None;
    1.18 +  in
    1.19 +    case result of
    1.20 +      None => Error (! buffer)
    1.21 +    | Some y => OK y
    1.22 +  end;
    1.23 +
    1.24 +
    1.25  (* read / write files *)
    1.26  
    1.27  fun read_file name =