src/Pure/library.ML
changeset 3699 7c30ab9e25d1
parent 3645 cfbd814a11f2
child 3762 f20b071a429a
     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 =