author | wenzelm |
Wed, 12 Mar 2025 11:39:00 +0100 | |
changeset 82265 | 4b875a4c83b0 |
parent 78764 | a3dcae9a2ebe |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62505
diff
changeset
|
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 |
||
62491 | 7 |
signature BASIC_EXN = |
8 |
sig |
|
9 |
exception ERROR of string |
|
10 |
val error: string -> 'a |
|
11 |
val cat_error: string -> string -> 'a |
|
12 |
end; |
|
13 |
||
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
14 |
signature EXN0 = |
28444 | 15 |
sig |
62491 | 16 |
include BASIC_EXN |
62821 | 17 |
val polyml_location: exn -> PolyML.location option |
62505 | 18 |
val reraise: exn -> 'a |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
19 |
datatype 'a result = Res of 'a | Exn of exn |
78674 | 20 |
val is_res: 'a result -> bool |
21 |
val is_exn: 'a result -> bool |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
22 |
val get_res: 'a result -> 'a option |
28444 | 23 |
val get_exn: 'a result -> exn option |
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
24 |
val capture0: ('a -> 'b) -> 'a -> 'b result (*unmanaged interrupts*) |
28444 | 25 |
val release: 'a result -> 'a |
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
26 |
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
|
27 |
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
|
28 |
val map_exn: (exn -> exn) -> 'a result -> 'a result |
78683 | 29 |
val cause: exn -> exn |
78764
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
30 |
exception Interrupt_Break |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
31 |
exception Interrupt_Breakdown |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
32 |
val is_interrupt_raw: exn -> bool |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
33 |
val is_interrupt_break: exn -> bool |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
34 |
val is_interrupt_breakdown: exn -> bool |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
35 |
val is_interrupt_proper: exn -> bool |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
36 |
val is_interrupt: exn -> bool |
78764
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
37 |
val is_interrupt_proper_exn: 'a result -> bool |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
38 |
val is_interrupt_exn: 'a result -> bool |
78705
fde0b195cb7d
clarified signature: avoid association with potentially dangerous Exn.capture;
wenzelm
parents:
78683
diff
changeset
|
39 |
val result: ('a -> 'b) -> 'a -> 'b result |
78673
90b12b919b5f
clarified signature (again): follow Isabelle/Java/Scala;
wenzelm
parents:
78671
diff
changeset
|
40 |
val failure_rc: exn -> int |
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
41 |
exception EXCEPTIONS of exn list |
62505 | 42 |
val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a |
28444 | 43 |
end; |
44 |
||
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
45 |
signature EXN = |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
46 |
sig |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
47 |
include EXN0 |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
48 |
val capture: ('a -> 'b) -> 'a -> 'b result (*managed interrupts*) |
78757 | 49 |
val capture_body: (unit -> 'a) -> 'a result |
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
50 |
end; |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
51 |
|
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
52 |
structure Exn: EXN0 = |
23962 | 53 |
struct |
54 |
||
62821 | 55 |
(* location *) |
62505 | 56 |
|
62821 | 57 |
val polyml_location = PolyML.Exception.exceptionLocation; |
58 |
||
59 |
val reraise = PolyML.Exception.reraise; |
|
62505 | 60 |
|
61 |
||
62492 | 62 |
(* user errors *) |
63 |
||
64 |
exception ERROR of string; |
|
65 |
||
66 |
fun error msg = raise ERROR msg; |
|
67 |
||
68 |
fun cat_error "" msg = error msg |
|
69 |
| cat_error msg "" = error msg |
|
70 |
| cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2); |
|
71 |
||
72 |
||
44158 | 73 |
(* exceptions as values *) |
28444 | 74 |
|
23962 | 75 |
datatype 'a result = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
76 |
Res of 'a | |
23962 | 77 |
Exn of exn; |
78 |
||
78674 | 79 |
fun is_res (Res _) = true |
80 |
| is_res _ = false; |
|
81 |
||
82 |
fun is_exn (Exn _) = true |
|
83 |
| is_exn _ = false; |
|
84 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
85 |
fun get_res (Res x) = SOME x |
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
86 |
| get_res _ = NONE; |
23962 | 87 |
|
88 |
fun get_exn (Exn exn) = SOME exn |
|
89 |
| get_exn _ = NONE; |
|
90 |
||
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78705
diff
changeset
|
91 |
fun capture0 f x = Res (f x) handle e => Exn e; |
23962 | 92 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
93 |
fun release (Res y) = y |
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
29564
diff
changeset
|
94 |
| release (Exn e) = reraise e; |
23962 | 95 |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
96 |
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
|
97 |
| 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
|
98 |
|
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
99 |
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
|
100 |
|
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
56667
diff
changeset
|
101 |
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
|
102 |
| map_exn f (Exn e) = Exn (f e); |
39472 | 103 |
|
28444 | 104 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
105 |
(* interrupts *) |
28444 | 106 |
|
78683 | 107 |
fun cause (IO.Io {cause = exn, ...}) = cause exn |
108 |
| cause exn = exn; |
|
109 |
||
78764
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
110 |
exception Interrupt_Break; |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
111 |
exception Interrupt_Breakdown; |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
112 |
|
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
113 |
fun is_interrupt_raw exn = (case cause exn of Thread.Thread.Interrupt => true | _ => false); |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
114 |
fun is_interrupt_break exn = (case cause exn of Interrupt_Break => true | _ => false); |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
115 |
fun is_interrupt_breakdown exn = (case cause exn of Interrupt_Breakdown => true | _ => false); |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
116 |
fun is_interrupt_proper exn = is_interrupt_raw exn orelse is_interrupt_break exn; |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
117 |
fun is_interrupt exn = is_interrupt_proper exn orelse is_interrupt_breakdown exn; |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
118 |
|
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
119 |
fun is_interrupt_proper_exn (Exn exn) = is_interrupt_proper exn |
a3dcae9a2ebe
distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents:
78757
diff
changeset
|
120 |
| is_interrupt_proper_exn _ = false; |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
121 |
|
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
122 |
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
|
123 |
| 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
|
124 |
|
78705
fde0b195cb7d
clarified signature: avoid association with potentially dangerous Exn.capture;
wenzelm
parents:
78683
diff
changeset
|
125 |
fun result f x = |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43537
diff
changeset
|
126 |
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
|
127 |
|
78673
90b12b919b5f
clarified signature (again): follow Isabelle/Java/Scala;
wenzelm
parents:
78671
diff
changeset
|
128 |
fun failure_rc exn = if is_interrupt exn then 130 else 2; |
90b12b919b5f
clarified signature (again): follow Isabelle/Java/Scala;
wenzelm
parents:
78671
diff
changeset
|
129 |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
130 |
|
44247 | 131 |
(* concatenated exceptions *) |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34136
diff
changeset
|
132 |
|
28459
f6a4d913cfb1
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents:
28444
diff
changeset
|
133 |
exception EXCEPTIONS of exn list; |
28444 | 134 |
|
62505 | 135 |
|
136 |
(* low-level trace *) |
|
137 |
||
138 |
fun trace exn_message output e = |
|
139 |
PolyML.Exception.traceException |
|
140 |
(e, fn (trace, exn) => |
|
141 |
let |
|
142 |
val title = "Exception trace - " ^ exn_message exn; |
|
143 |
val () = output (String.concatWith "\n" (title :: trace)); |
|
144 |
in reraise exn end); |
|
145 |
||
23962 | 146 |
end; |