1(*  Title:      Pure/General/exn.ML
2    Author:     Makarius
3
4Support for exceptions.
5*)
6
7signature Exn =
8sig
9  exception ERROR of string
10  val error: string -> 'a
11  val cat_error: string -> string -> 'a
12  val polyml_location: exn -> PolyML.location option
13  val reraise: exn -> 'a
14  datatype 'a result = Res of 'a | Exn of exn
15  val get_res: 'a result -> 'a option
16  val get_exn: 'a result -> exn option
17  val capture: ('a -> 'b) -> 'a -> 'b result
18  val release: 'a result -> 'a
19  val map_res: ('a -> 'b) -> 'a result -> 'b result
20  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
21  val map_exn: (exn -> exn) -> 'a result -> 'a result
22  exception Interrupt
23  val interrupt: unit -> 'a
24  val is_interrupt: exn -> bool
25  val interrupt_exn: 'a result
26  val is_interrupt_exn: 'a result -> bool
27  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
28  exception EXCEPTIONS of exn list
29  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
30end
31