1(*  Title:      Pure/General/exn.ML
2    Author:     Makarius
3
4Support for exceptions.
5*)
6
7signature BASIC_EXN =
8sig
9  exception ERROR of string
10  val error: string -> 'a
11  val cat_error: string -> string -> 'a
12end;
13
14signature EXN =
15sig
16  include BASIC_EXN
17  val polyml_location: exn -> PolyML.location option
18  val reraise: exn -> 'a
19  datatype 'a result = Res of 'a | Exn of exn
20  val get_res: 'a result -> 'a option
21  val get_exn: 'a result -> exn option
22  val capture: ('a -> 'b) -> 'a -> 'b result
23  val release: 'a result -> 'a
24  val map_res: ('a -> 'b) -> 'a result -> 'b result
25  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
26  val map_exn: (exn -> exn) -> 'a result -> 'a result
27  exception Interrupt
28  val interrupt: unit -> 'a
29  val is_interrupt: exn -> bool
30  val interrupt_exn: 'a result
31  val is_interrupt_exn: 'a result -> bool
32  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
33  val return_code: exn -> int -> int
34  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
35  exception EXCEPTIONS of exn list
36  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
37end;
38
39structure Exn: EXN =
40struct
41
42(* location *)
43
44val polyml_location = PolyML.Exception.exceptionLocation;
45
46val reraise = PolyML.Exception.reraise;
47
48
49(* user errors *)
50
51exception ERROR of string;
52
53fun error msg = raise ERROR msg;
54
55fun cat_error "" msg = error msg
56  | cat_error msg "" = error msg
57  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
58
59
60(* exceptions as values *)
61
62datatype 'a result =
63  Res of 'a |
64  Exn of exn;
65
66fun get_res (Res x) = SOME x
67  | get_res _ = NONE;
68
69fun get_exn (Exn exn) = SOME exn
70  | get_exn _ = NONE;
71
72fun capture f x = Res (f x) handle e => Exn e;
73
74fun release (Res y) = y
75  | release (Exn e) = reraise e;
76
77fun map_res f (Res x) = Res (f x)
78  | map_res f (Exn e) = Exn e;
79
80fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
81
82fun map_exn f (Res x) = Res x
83  | map_exn f (Exn e) = Exn (f e);
84
85
86(* interrupts *)
87
88exception Interrupt = Thread.Thread.Interrupt;
89
90fun interrupt () = raise Interrupt;
91
92fun is_interrupt Interrupt = true
93  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
94  | is_interrupt _ = false;
95
96val interrupt_exn = Exn Interrupt;
97
98fun is_interrupt_exn (Exn exn) = is_interrupt exn
99  | is_interrupt_exn _ = false;
100
101fun interruptible_capture f x =
102  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
103
104
105(* POSIX return code *)
106
107fun return_code exn rc =
108  if is_interrupt exn then (130: int) else rc;
109
110fun capture_exit rc f x =
111  f x handle exn => exit (return_code exn rc);
112
113
114(* concatenated exceptions *)
115
116exception EXCEPTIONS of exn list;
117
118
119(* low-level trace *)
120
121fun trace exn_message output e =
122  PolyML.Exception.traceException
123    (e, fn (trace, exn) =>
124      let
125        val title = "Exception trace - " ^ exn_message exn;
126        val () = output (String.concatWith "\n" (title :: trace));
127      in reraise exn end);
128
129end;
130