1(*  Title:      Pure/General/exn.ML
2    Author:     Makarius
3
4Support for exceptions.
5*)
6
7structure Exn: Exn =
8struct
9
10(* location *)
11
12val polyml_location = PolyML.Exception.exceptionLocation;
13
14val reraise = PolyML.Exception.reraise;
15
16
17(* user errors *)
18
19exception ERROR of string;
20
21fun error msg = raise ERROR msg;
22
23fun cat_error "" msg = error msg
24  | cat_error msg "" = error msg
25  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
26
27
28(* exceptions as values *)
29
30datatype 'a result =
31  Res of 'a |
32  Exn of exn;
33
34fun get_res (Res x) = SOME x
35  | get_res _ = NONE;
36
37fun get_exn (Exn exn) = SOME exn
38  | get_exn _ = NONE;
39
40fun capture f x = Res (f x) handle e => Exn e;
41
42fun release (Res y) = y
43  | release (Exn e) = reraise e;
44
45fun map_res f (Res x) = Res (f x)
46  | map_res f (Exn e) = Exn e;
47
48fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
49
50fun map_exn f (Res x) = Res x
51  | map_exn f (Exn e) = Exn (f e);
52
53
54(* interrupts *)
55
56exception Interrupt = Thread.Thread.Interrupt;
57
58fun interrupt () = raise Interrupt;
59
60fun is_interrupt Interrupt = true
61  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
62  | is_interrupt _ = false;
63
64val interrupt_exn = Exn Interrupt;
65
66fun is_interrupt_exn (Exn exn) = is_interrupt exn
67  | is_interrupt_exn _ = false;
68
69fun interruptible_capture f x =
70  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
71
72
73(* concatenated exceptions *)
74
75exception EXCEPTIONS of exn list;
76
77
78(* low-level trace *)
79
80fun trace exn_message output e =
81  PolyML.Exception.traceException
82    (e, fn (trace, exn) =>
83      let
84        val title = "Exception trace - " ^ exn_message exn;
85        val () = output (String.concatWith "\n" (title :: trace));
86      in reraise exn end);
87
88end;
89