author | Manuel Eberl <eberlm@in.tum.de> |
Tue, 19 Jan 2016 11:19:25 +0100 | |
changeset 62201 | eca7b38c8ee5 |
parent 62198 | 7217adc19be9 |
child 62491 | 7187cb7a77c5 |
permissions | -rw-r--r-- |
61925 | 1 |
(* Title: Pure/RAW/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 |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
14 |
val map_res: ('a -> 'b) -> 'a result -> 'b result |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
15 |
val maps_res: ('a -> 'b result) -> 'a result -> 'b result |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
16 |
val map_exn: (exn -> exn) -> 'a result -> 'a result |
28444 | 17 |
exception Interrupt |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
val interruptible_capture: ('a -> 'b) -> 'a -> 'b result |
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
56628
diff
changeset
|
23 |
val return_code: exn -> int -> int |
56628 | 24 |
val capture_exit: int -> ('a -> 'b) -> 'a -> 'b |
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
25 |
exception EXCEPTIONS of exn list |
28444 | 26 |
end; |
27 |
||
28 |
structure Exn: EXN = |
|
23962 | 29 |
struct |
30 |
||
44158 | 31 |
(* exceptions as values *) |
28444 | 32 |
|
23962 | 33 |
datatype 'a result = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
34 |
Res of 'a | |
23962 | 35 |
Exn of exn; |
36 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
37 |
fun get_res (Res x) = SOME x |
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
38 |
| get_res _ = NONE; |
23962 | 39 |
|
40 |
fun get_exn (Exn exn) = SOME exn |
|
41 |
| get_exn _ = NONE; |
|
42 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
43 |
fun capture f x = Res (f x) handle e => Exn e; |
23962 | 44 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
45 |
fun release (Res y) = y |
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
29564
diff
changeset
|
46 |
| release (Exn e) = reraise e; |
23962 | 47 |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
48 |
fun map_res f (Res x) = Res (f x) |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
49 |
| map_res f (Exn e) = Exn e; |
42223
098c86e53153
more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents:
40483
diff
changeset
|
50 |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
51 |
fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f; |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
52 |
|
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
53 |
fun map_exn f (Res x) = Res x |
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
54 |
| map_exn f (Exn e) = Exn (f e); |
39472 | 55 |
|
28444 | 56 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
57 |
(* interrupts *) |
28444 | 58 |
|
59 |
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
|
60 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
61 |
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
|
62 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
63 |
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
|
64 |
| 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
|
65 |
| is_interrupt _ = false; |
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 |
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
|
68 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
69 |
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
|
70 |
| 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
|
71 |
|
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 |
fun interruptible_capture f x = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
73 |
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
|
74 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
75 |
|
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
56628
diff
changeset
|
76 |
(* POSIX return code *) |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
56628
diff
changeset
|
77 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
56628
diff
changeset
|
78 |
fun return_code exn rc = |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
56628
diff
changeset
|
79 |
if is_interrupt exn then (130: int) else rc; |
56628 | 80 |
|
81 |
fun capture_exit rc f x = |
|
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
56628
diff
changeset
|
82 |
f x handle exn => exit (return_code exn rc); |
56628 | 83 |
|
84 |
||
44247 | 85 |
(* concatenated exceptions *) |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
86 |
|
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
87 |
exception EXCEPTIONS of exn list; |
28444 | 88 |
|
23962 | 89 |
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
|
90 |
|
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
|
91 |
datatype illegal = Interrupt; |