# HG changeset patch
# User wenzelm
# Date 1222855204 -7200
# Node ID 283d5e41953dd28a0f68309e9f064cab575d8073
# Parent  de653f1ad78b4b322d03dca00a59ab6fba33a2c1
more robust treatment of Interrupt;
added release_all, release_first;
proper signature;

diff -r de653f1ad78b -r 283d5e41953d src/Pure/ML-Systems/exn.ML
--- a/src/Pure/ML-Systems/exn.ML	Wed Oct 01 12:00:02 2008 +0200
+++ b/src/Pure/ML-Systems/exn.ML	Wed Oct 01 12:00:04 2008 +0200
@@ -2,12 +2,28 @@
     ID:         $Id$
     Author:     Makarius
 
-Runtime exceptions as values.
+Extra support for exceptions.
 *)
 
-structure Exn =
+signature EXN =
+sig
+  datatype 'a result = Exn of exn | Result of 'a
+  val get_result: 'a result -> 'a option
+  val get_exn: 'a result -> exn option
+  val capture: ('a -> 'b) -> 'a -> 'b result
+  val release: 'a result -> 'a
+  exception Interrupt
+  val proper_exn: 'a result -> exn option
+  exception EXCEPTIONS of exn list * string
+  val release_all: 'a result list -> 'a list
+  val release_first: 'a result list -> 'a list
+end;
+
+structure Exn: EXN =
 struct
 
+(* runtime exceptions as values *)
+
 datatype 'a result =
   Result of 'a |
   Exn of exn;
@@ -23,6 +39,29 @@
 fun release (Result y) = y
   | release (Exn e) = raise e;
 
+
+(* interrupt *)
+
+exception Interrupt = Interrupt;
+
+fun proper_exn (Result _) = NONE
+  | proper_exn (Exn Interrupt) = NONE
+  | proper_exn (Exn exn) = SOME exn;
+
+
+(* release results -- collating interrupts *)
+
 exception EXCEPTIONS of exn list * string;
 
+fun release_all results =
+  if List.all (fn Result _ => true | _ => false) results
+  then map (fn Result x => x) results
+  else
+    (case List.mapPartial proper_exn results of
+      [] => raise Interrupt
+    | exns => raise EXCEPTIONS (exns, ""));
+
+fun release_first results = release_all results
+  handle EXCEPTIONS (exn :: _, _) => raise exn;
+
 end;