src/Pure/library.ML
changeset 5037 224887671646
parent 4995 905cd6f73429
child 5112 9e74cf11e4a4
     1.1 --- a/src/Pure/library.ML	Sat Jun 13 18:25:39 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Jun 15 11:05:25 1998 +0200
     1.3 @@ -1038,7 +1038,7 @@
     1.4  
     1.5  (*print error message and abort to top level*)
     1.6  exception ERROR;
     1.7 -fun error_msg s = !error_fn s;	  (*promise to raise ERROR later!*)
     1.8 +fun error_msg s = !error_fn s;
     1.9  fun error s = (error_msg s; raise ERROR);
    1.10  fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
    1.11  
    1.12 @@ -1064,19 +1064,24 @@
    1.13  fun get_ok (OK x) = Some x
    1.14    | get_ok _ = None;
    1.15  
    1.16 +datatype 'a result =
    1.17 +  Result of 'a |
    1.18 +  Exn of exn;
    1.19 +
    1.20  fun handle_error f x =
    1.21    let
    1.22      val buffer = ref ([]: string list);
    1.23      fun capture s = buffer := ! buffer @ [s];
    1.24 -    val result = Some (setmp error_fn capture f x) handle ERROR => None;
    1.25 +    fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
    1.26    in
    1.27 -    (case result of
    1.28 -      None => Error (cat_lines (! buffer))
    1.29 -    | Some y => OK y)
    1.30 +    (case Result (setmp error_fn capture f x) handle exn => Exn exn of
    1.31 +      Result y => (err_msg (); OK y)
    1.32 +    | Exn ERROR => Error (cat_lines (! buffer))
    1.33 +    | Exn exn => (err_msg (); raise exn))
    1.34    end;
    1.35  
    1.36  
    1.37 -(* transform ERROR into ERROR_MESSAGE, capturing the side-effect *)
    1.38 +(* transform ERROR into ERROR_MESSAGE *)
    1.39  
    1.40  exception ERROR_MESSAGE of string;
    1.41