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