23962
|
1 |
(* Title: Pure/ML-Systems/exn.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
28444
|
5 |
Extra support for exceptions.
|
23962
|
6 |
*)
|
|
7 |
|
28444
|
8 |
signature EXN =
|
|
9 |
sig
|
|
10 |
datatype 'a result = Exn of exn | Result of 'a
|
|
11 |
val get_result: 'a result -> 'a option
|
|
12 |
val get_exn: 'a result -> exn option
|
|
13 |
val capture: ('a -> 'b) -> 'a -> 'b result
|
|
14 |
val release: 'a result -> 'a
|
|
15 |
exception Interrupt
|
|
16 |
val proper_exn: 'a result -> exn option
|
|
17 |
exception EXCEPTIONS of exn list * string
|
|
18 |
val release_all: 'a result list -> 'a list
|
|
19 |
val release_first: 'a result list -> 'a list
|
|
20 |
end;
|
|
21 |
|
|
22 |
structure Exn: EXN =
|
23962
|
23 |
struct
|
|
24 |
|
28444
|
25 |
(* runtime exceptions as values *)
|
|
26 |
|
23962
|
27 |
datatype 'a result =
|
|
28 |
Result of 'a |
|
|
29 |
Exn of exn;
|
|
30 |
|
|
31 |
fun get_result (Result x) = SOME x
|
|
32 |
| get_result _ = NONE;
|
|
33 |
|
|
34 |
fun get_exn (Exn exn) = SOME exn
|
|
35 |
| get_exn _ = NONE;
|
|
36 |
|
|
37 |
fun capture f x = Result (f x) handle e => Exn e;
|
|
38 |
|
|
39 |
fun release (Result y) = y
|
|
40 |
| release (Exn e) = raise e;
|
|
41 |
|
28444
|
42 |
|
|
43 |
(* interrupt *)
|
|
44 |
|
|
45 |
exception Interrupt = Interrupt;
|
|
46 |
|
|
47 |
fun proper_exn (Result _) = NONE
|
|
48 |
| proper_exn (Exn Interrupt) = NONE
|
|
49 |
| proper_exn (Exn exn) = SOME exn;
|
|
50 |
|
|
51 |
|
|
52 |
(* release results -- collating interrupts *)
|
|
53 |
|
23962
|
54 |
exception EXCEPTIONS of exn list * string;
|
|
55 |
|
28444
|
56 |
fun release_all results =
|
|
57 |
if List.all (fn Result _ => true | _ => false) results
|
|
58 |
then map (fn Result x => x) results
|
|
59 |
else
|
|
60 |
(case List.mapPartial proper_exn results of
|
|
61 |
[] => raise Interrupt
|
|
62 |
| exns => raise EXCEPTIONS (exns, ""));
|
|
63 |
|
|
64 |
fun release_first results = release_all results
|
|
65 |
handle EXCEPTIONS (exn :: _, _) => raise exn;
|
|
66 |
|
23962
|
67 |
end;
|