author | wenzelm |
Wed, 17 Aug 2011 20:08:36 +0200 | |
changeset 44246 | 380a4677c55d |
parent 44158 | fe6d1ae7a065 |
child 44247 | 270366301bd7 |
permissions | -rw-r--r-- |
34136 | 1 |
(* Title: Pure/General/exn.ML |
23962 | 2 |
Author: Makarius |
3 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
4 |
Support for exceptions. |
23962 | 5 |
*) |
6 |
||
28444 | 7 |
signature EXN = |
8 |
sig |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
9 |
datatype 'a result = Res of 'a | Exn of exn |
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
10 |
val get_res: 'a result -> 'a option |
28444 | 11 |
val get_exn: 'a result -> exn option |
12 |
val capture: ('a -> 'b) -> 'a -> 'b result |
|
13 |
val release: 'a result -> 'a |
|
40234
39af96cc57cb
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents:
39472
diff
changeset
|
14 |
val map_result: ('a -> 'b) -> 'a result -> 'b result |
42223
098c86e53153
more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents:
40483
diff
changeset
|
15 |
val maps_result: ('a -> 'b result) -> 'a result -> 'b result |
28444 | 16 |
exception Interrupt |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
17 |
val interrupt: unit -> 'a |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
18 |
val is_interrupt: exn -> bool |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
19 |
val interrupt_exn: 'a result |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
20 |
val is_interrupt_exn: 'a result -> bool |
40234
39af96cc57cb
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents:
39472
diff
changeset
|
21 |
val interruptible_capture: ('a -> 'b) -> 'a -> 'b result |
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
22 |
exception EXCEPTIONS of exn list |
32100
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
23 |
val flatten: exn -> exn list |
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
24 |
val flatten_list: exn list -> exn list |
28444 | 25 |
val release_all: 'a result list -> 'a list |
26 |
val release_first: 'a result list -> 'a list |
|
27 |
end; |
|
28 |
||
29 |
structure Exn: EXN = |
|
23962 | 30 |
struct |
31 |
||
44158 | 32 |
(* exceptions as values *) |
28444 | 33 |
|
23962 | 34 |
datatype 'a result = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
35 |
Res of 'a | |
23962 | 36 |
Exn of exn; |
37 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
38 |
fun get_res (Res x) = SOME x |
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
39 |
| get_res _ = NONE; |
23962 | 40 |
|
41 |
fun get_exn (Exn exn) = SOME exn |
|
42 |
| get_exn _ = NONE; |
|
43 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
44 |
fun capture f x = Res (f x) handle e => Exn e; |
23962 | 45 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
46 |
fun release (Res y) = y |
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
29564
diff
changeset
|
47 |
| release (Exn e) = reraise e; |
23962 | 48 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
49 |
fun map_result f (Res x) = Res (f x) |
42223
098c86e53153
more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents:
40483
diff
changeset
|
50 |
| map_result f (Exn e) = Exn e; |
098c86e53153
more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents:
40483
diff
changeset
|
51 |
|
44246 | 52 |
fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f; |
39472 | 53 |
|
28444 | 54 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
55 |
(* interrupts *) |
28444 | 56 |
|
57 |
exception Interrupt = Interrupt; |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
58 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
59 |
fun interrupt () = raise Interrupt; |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
60 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
61 |
fun is_interrupt Interrupt = true |
40234
39af96cc57cb
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents:
39472
diff
changeset
|
62 |
| is_interrupt (IO.Io {cause, ...}) = is_interrupt cause |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
63 |
| is_interrupt _ = false; |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
64 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
65 |
val interrupt_exn = Exn Interrupt; |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
66 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
67 |
fun is_interrupt_exn (Exn exn) = is_interrupt exn |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
68 |
| is_interrupt_exn _ = false; |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
69 |
|
40234
39af96cc57cb
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents:
39472
diff
changeset
|
70 |
fun interruptible_capture f x = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
71 |
Res (f x) handle e => if is_interrupt e then reraise e else Exn e; |
40234
39af96cc57cb
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents:
39472
diff
changeset
|
72 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
73 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
74 |
(* nested exceptions *) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
75 |
|
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
76 |
exception EXCEPTIONS of exn list; |
28444 | 77 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
78 |
fun flatten (EXCEPTIONS exns) = flatten_list exns |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
79 |
| flatten exn = if is_interrupt exn then [] else [exn] |
32100
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
80 |
and flatten_list exns = List.concat (map flatten exns); |
23962 | 81 |
|
28444 | 82 |
fun release_all results = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
83 |
if List.all (fn Res _ => true | _ => false) results |
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
84 |
then map (fn Res x => x) results |
32100
8ac6b1102f16
added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents:
31427
diff
changeset
|
85 |
else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results)); |
28444 | 86 |
|
87 |
fun release_first results = release_all results |
|
43537
80803078552e
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
wenzelm
parents:
42223
diff
changeset
|
88 |
handle EXCEPTIONS [] => interrupt () |
80803078552e
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
wenzelm
parents:
42223
diff
changeset
|
89 |
| EXCEPTIONS (exn :: _) => reraise exn; |
28444 | 90 |
|
23962 | 91 |
end; |
40483
3848283c14bb
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm
parents:
40234
diff
changeset
|
92 |
|
3848283c14bb
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm
parents:
40234
diff
changeset
|
93 |
datatype illegal = Interrupt; |
3848283c14bb
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm
parents:
40234
diff
changeset
|
94 |