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