author | wenzelm |
Sat, 21 Nov 2009 17:01:44 +0100 | |
changeset 33834 | 7c06e19f717c |
parent 32100 | 8ac6b1102f16 |
permissions | -rw-r--r-- |
23962 | 1 |
(* Title: Pure/ML-Systems/exn.ML |
2 |
Author: Makarius |
|
3 |
||
28444 | 4 |
Extra support for exceptions. |
23962 | 5 |
*) |
6 |
||
28444 | 7 |
signature EXN = |
8 |
sig |
|
9 |
datatype 'a result = Exn of exn | Result of 'a |
|
10 |
val get_result: 'a result -> 'a option |
|
11 |
val get_exn: 'a result -> exn option |
|
12 |
val capture: ('a -> 'b) -> 'a -> 'b result |
|
13 |
val release: 'a result -> 'a |
|
14 |
exception Interrupt |
|
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
15 |
exception EXCEPTIONS of exn list |
32100
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
16 |
val flatten: exn -> exn list |
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
17 |
val flatten_list: exn list -> exn list |
28444 | 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 |
|
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
29564
diff
changeset
|
40 |
| release (Exn e) = reraise e; |
23962 | 41 |
|
28444 | 42 |
|
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
43 |
(* interrupt and nested exceptions *) |
28444 | 44 |
|
45 |
exception Interrupt = Interrupt; |
|
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
46 |
exception EXCEPTIONS of exn list; |
28444 | 47 |
|
32100
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
48 |
fun flatten Interrupt = [] |
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
49 |
| flatten (EXCEPTIONS exns) = flatten_list exns |
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
50 |
| flatten exn = [exn] |
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
51 |
and flatten_list exns = List.concat (map flatten exns); |
23962 | 52 |
|
28444 | 53 |
fun release_all results = |
54 |
if List.all (fn Result _ => true | _ => false) results |
|
55 |
then map (fn Result x => x) results |
|
32100
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
56 |
else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results)); |
28444 | 57 |
|
58 |
fun release_first results = release_all results |
|
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
29564
diff
changeset
|
59 |
handle EXCEPTIONS (exn :: _) => reraise exn; |
28444 | 60 |
|
23962 | 61 |
end; |