src/Pure/ML-Systems/exn.ML
changeset 28459 f6a4d913cfb1
parent 28444 283d5e41953d
child 29564 f8b933a62151
     1.1 --- a/src/Pure/ML-Systems/exn.ML	Thu Oct 02 14:22:40 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/exn.ML	Thu Oct 02 14:22:44 2008 +0200
     1.3 @@ -13,8 +13,7 @@
     1.4    val capture: ('a -> 'b) -> 'a -> 'b result
     1.5    val release: 'a result -> 'a
     1.6    exception Interrupt
     1.7 -  val proper_exn: 'a result -> exn option
     1.8 -  exception EXCEPTIONS of exn list * string
     1.9 +  exception EXCEPTIONS of exn list
    1.10    val release_all: 'a result list -> 'a list
    1.11    val release_first: 'a result list -> 'a list
    1.12  end;
    1.13 @@ -40,28 +39,26 @@
    1.14    | release (Exn e) = raise e;
    1.15  
    1.16  
    1.17 -(* interrupt *)
    1.18 +(* interrupt and nested exceptions *)
    1.19  
    1.20  exception Interrupt = Interrupt;
    1.21 -
    1.22 -fun proper_exn (Result _) = NONE
    1.23 -  | proper_exn (Exn Interrupt) = NONE
    1.24 -  | proper_exn (Exn exn) = SOME exn;
    1.25 +exception EXCEPTIONS of exn list;
    1.26  
    1.27 +fun plain_exns (Result _) = []
    1.28 +  | plain_exns (Exn Interrupt) = []
    1.29 +  | plain_exns (Exn (EXCEPTIONS exns)) = List.concat (map (plain_exns o Exn) exns)
    1.30 +  | plain_exns (Exn exn) = [exn];
    1.31  
    1.32 -(* release results -- collating interrupts *)
    1.33 -
    1.34 -exception EXCEPTIONS of exn list * string;
    1.35  
    1.36  fun release_all results =
    1.37    if List.all (fn Result _ => true | _ => false) results
    1.38    then map (fn Result x => x) results
    1.39    else
    1.40 -    (case List.mapPartial proper_exn results of
    1.41 +    (case List.concat (map plain_exns results) of
    1.42        [] => raise Interrupt
    1.43 -    | exns => raise EXCEPTIONS (exns, ""));
    1.44 +    | exns => raise EXCEPTIONS exns);
    1.45  
    1.46  fun release_first results = release_all results
    1.47 -  handle EXCEPTIONS (exn :: _, _) => raise exn;
    1.48 +  handle EXCEPTIONS (exn :: _) => raise exn;
    1.49  
    1.50  end;