src/Pure/ML-Systems/exn.ML
changeset 28444 283d5e41953d
parent 23962 e0358fac0541
child 28459 f6a4d913cfb1
     1.1 --- a/src/Pure/ML-Systems/exn.ML	Wed Oct 01 12:00:02 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/exn.ML	Wed Oct 01 12:00:04 2008 +0200
     1.3 @@ -2,12 +2,28 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Runtime exceptions as values.
     1.8 +Extra support for exceptions.
     1.9  *)
    1.10  
    1.11 -structure Exn =
    1.12 +signature EXN =
    1.13 +sig
    1.14 +  datatype 'a result = Exn of exn | Result of 'a
    1.15 +  val get_result: 'a result -> 'a option
    1.16 +  val get_exn: 'a result -> exn option
    1.17 +  val capture: ('a -> 'b) -> 'a -> 'b result
    1.18 +  val release: 'a result -> 'a
    1.19 +  exception Interrupt
    1.20 +  val proper_exn: 'a result -> exn option
    1.21 +  exception EXCEPTIONS of exn list * string
    1.22 +  val release_all: 'a result list -> 'a list
    1.23 +  val release_first: 'a result list -> 'a list
    1.24 +end;
    1.25 +
    1.26 +structure Exn: EXN =
    1.27  struct
    1.28  
    1.29 +(* runtime exceptions as values *)
    1.30 +
    1.31  datatype 'a result =
    1.32    Result of 'a |
    1.33    Exn of exn;
    1.34 @@ -23,6 +39,29 @@
    1.35  fun release (Result y) = y
    1.36    | release (Exn e) = raise e;
    1.37  
    1.38 +
    1.39 +(* interrupt *)
    1.40 +
    1.41 +exception Interrupt = Interrupt;
    1.42 +
    1.43 +fun proper_exn (Result _) = NONE
    1.44 +  | proper_exn (Exn Interrupt) = NONE
    1.45 +  | proper_exn (Exn exn) = SOME exn;
    1.46 +
    1.47 +
    1.48 +(* release results -- collating interrupts *)
    1.49 +
    1.50  exception EXCEPTIONS of exn list * string;
    1.51  
    1.52 +fun release_all results =
    1.53 +  if List.all (fn Result _ => true | _ => false) results
    1.54 +  then map (fn Result x => x) results
    1.55 +  else
    1.56 +    (case List.mapPartial proper_exn results of
    1.57 +      [] => raise Interrupt
    1.58 +    | exns => raise EXCEPTIONS (exns, ""));
    1.59 +
    1.60 +fun release_first results = release_all results
    1.61 +  handle EXCEPTIONS (exn :: _, _) => raise exn;
    1.62 +
    1.63  end;